diff options
| -rw-r--r-- | .circleci/config.yml | 105 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 202 | ||||
| -rw-r--r-- | .travis.yml | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 1 | ||||
| -rw-r--r-- | dev/ci/docker/README.md | 65 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 45 | ||||
| -rwxr-xr-x | dev/ci/docker/bionic_coq/hooks/post_push | 8 |
7 files changed, 172 insertions, 260 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 451b711be..07b728edf 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -8,83 +8,29 @@ defaults: # reference syntax) working_directory: ~/coq docker: - - image: ocaml/opam:ubuntu + - image: coqci/base:V2018-05-05 environment: &envvars - # required by some of the targets, e.g. compcert, passed for - # instance to opam to configure the number of parallel jobs - # allowed - NJOBS: 2 - COMPILER: "system" - CAMLP5_VER: "6.14" NATIVE_COMP: "yes" - # some useful values - TIMING_PACKAGES: &timing-packages "time python" - version: 2 before_script: &before_script - name: Install system packages + name: Setup OPAM Switch command: | echo export TERM=xterm >> ~/.profile source ~/.profile - printenv - if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi echo . ~/.profile >> $BASH_ENV - -opam-switch: &opam-switch - name: Select opam switch - command: | - opam switch ${COMPILER} + printenv | sort + opam switch "$COMPILER" opam config list opam list -.opam-boot-template: &opam-boot-template - <<: *params - steps: - - checkout - - run: *before_script - - run: - name: Cache selection - command: | - # We can't use environment variables in cache names - # So put it in a file and use the checksum - echo "$COMPILER" > COMPILER - - restore_cache: - keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- - - run: - name: Update opam lists - command: | - opam repository set-url default https://opam.ocaml.org - opam update - - run: - name: Install opam packages - command: | - opam switch -j ${NJOBS} ${COMPILER} - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} - - run: - name: Clean cache - command: | - rm -rf ~/.opam/log/ - - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- - paths: - - ~/.opam - - persist_to_workspace: - root: &workspace ~/ - paths: - - .opam/ - .build-template: &build-template <<: *params steps: - checkout - run: *before_script - - attach_workspace: &attach_workspace - at: *workspace - - run: *opam-switch - run: &build-configure name: Configure command: | @@ -96,7 +42,7 @@ opam-switch: &opam-switch make -j ${NJOBS} make test-suite/misc/universes/all_stdlib.v - persist_to_workspace: - root: *workspace + root: &workspace ~/ paths: - coq/ @@ -106,7 +52,9 @@ opam-switch: &opam-switch <<: *params steps: - run: *before_script - - attach_workspace: *attach_workspace + - attach_workspace: &attach_workspace + at: *workspace + - run: name: Test command: | @@ -115,19 +63,10 @@ opam-switch: &opam-switch root: *workspace paths: - coq/ - environment: &ci-template-vars - <<: *envvars - EXTRA_PACKAGES: *timing-packages # Defines individual jobs, see the workflows section below for job orchestration jobs: - opam-boot: - <<: *opam-boot-template - environment: - <<: *envvars - EXTRA_OPAM: "ocamlgraph elpi" - # Build and prepare test environment build: *build-template @@ -136,24 +75,15 @@ jobs: color: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: *timing-packages compcert: <<: *ci-template coq-dpdgraph: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" coquelicot: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" elpi: <<: *ci-template @@ -172,15 +102,9 @@ jobs: fiat-parsers: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: *timing-packages flocq: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" math-classes: <<: *ci-template @@ -193,9 +117,6 @@ jobs: hott: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" iris-lambda-rust: <<: *ci-template @@ -214,9 +135,6 @@ jobs: sf: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python wget" unimath: <<: *ci-template @@ -226,14 +144,11 @@ jobs: workflows: version: 2 + # Run on each push main: jobs: - - opam-boot - - - build: - requires: - - opam-boot + - build - bignums: &req-main requires: diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d16dc5b78..12d3a87b2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,76 +1,35 @@ -image: ubuntu:bionic +image: coqci/base:V2018-05-05 stages: - - opam-boot - build - test # some default values variables: - # Format: $IMAGE-V$DATE-$HOUR-$MINUTE - CACHEKEY: bionic-V2018-04-29-00-50 - DEBIAN_FRONTEND: "noninteractive" - NJOBS: "2" - COMPILER: "4.02.3" - CAMLP5_VER: "6.14" - OPAMROOT: "$CI_PROJECT_DIR/.opamcache" - OPAMROOTISOK: "true" - - # some useful values - COMPILER_32BIT: "4.02.3+32bit" - - COMPILER_BLEEDING_EDGE: "4.06.1" - CAMLP5_VER_BLEEDING_EDGE: "7.05" - - TIMING_PACKAGES: "time python3" - - COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" - #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" - COQIDE_OPAM: "lablgtk.2.18.5 conf-gtksourceview.2" - COQIDE_OPAM_BE: "lablgtk.2.18.6 conf-gtksourceview.2" - COQDOC_PACKAGES: "texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip" - SPHINX_PACKAGES: "antlr4-python3-runtime" - ELPI_OPAM: "elpi" + # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here + # for reference] + CACHEKEY: bionic_coq-V2018-05-03 + # By default, jobs run in the base switch; override to select another switch + OPAM_SWITCH: "base" + # Used to select special compiler switches such as flambda, 32bits, etc... + OPAM_VARIANT: "" before_script: - cat /proc/{cpu,mem}info || true - ls -a # figure out if artifacts are around - - printenv -# - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi - - apt-get update -qq && apt-get install -y -qq m4 opam ${EXTRA_PACKAGES} - # This should be replaced by standard debian packages once python3-antlr4 makes to the archive. - - if [ -n "${PIP_PACKAGES}" ]; then pip3 install ${PIP_PACKAGES}; fi - # if no cache running opam config fails! - - if [ -d .opamcache ]; then eval $(opam config env); fi - -################ OPAM SYSTEM ###################### -# - use cache between pipelines -# - use artifacts between jobs -# (in https://gitlab.com/SkySkimmer/coq/-/jobs/63255417 -# the cache wasn't available at the build step) -# every non opam-boot job must set dependencies (for ci it's in the template) -# otherwise all opam-boot artifacts are used together and we get some random switch - -# set cache key when using -.opam-boot-template: &opam-boot-template - stage: opam-boot - artifacts: - name: "opam-$COMPILER" - paths: - - .opamcache - expire_in: 1 week - script: - - opam init -a -y -j $NJOBS --compiler=${COMPILER} default https://opam.ocaml.org - - eval $(opam config env) - - opam update - - opam config list - - opam list - - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM} - - rm -rf ~/.opam/log/ - - opam list - -# TODO figure out how to build doc for installed coq -# set dependencies when using + - printenv | sort + - declare -A switch_table + - switch_table=( ["base"]="$COMPILER" ["be"]="$COMPILER_BE" ) + - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT" + - eval $(opam config env) + - opam list + - opam config list + +################ GITLAB CACHING ###################### +# - use artifacts between jobs # +###################################################### + +# TODO figure out how to build doc for installed Coq .build-template: &build-template stage: build artifacts: @@ -80,21 +39,16 @@ before_script: - config/Makefile - test-suite/misc/universes/all_stdlib.v expire_in: 1 week - dependencies: - - not-a-real-job script: - set -e - - printenv - - opam config list - - opam list - echo 'start:coq.config' - ./configure -prefix "$(pwd)/_install_ci" ${EXTRA_CONF} - echo 'end:coq.config' - echo 'start:coq.build' - - make -j ${NJOBS} byte - - make -j ${NJOBS} + - make -j "$NJOBS" byte + - make -j "$NJOBS" - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' @@ -106,12 +60,9 @@ before_script: - set +e -# set dependencies when using .warnings-template: &warnings-template # keep warnings in test stage so we can test things even when warnings occur stage: test - dependencies: - - not-a-real-job script: - set -e @@ -120,14 +71,17 @@ before_script: - echo 'end:coq.config' - echo 'start:coq.build' - - make -j ${NJOBS} coqocaml + - make -j "$NJOBS" coqocaml - echo 'end:coq:build' - set +e variables: &warnings-variables EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" - EXTRA_PACKAGES: "$COQIDE_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM" + +# every non build job must set dependencies otherwise all build +# artifacts are used together and we may get some random Coq. To that +# purpose, we add a spurious dependency `not-a-real-job` that must be +# overridden otherwise the CI will fail. # set dependencies when using .test-suite-template: &test-suite-template @@ -140,7 +94,7 @@ before_script: # careful with the ending / - BIN=$(readlink -f ../_install_ci/bin)/ - LIB=$(readlink -f ../_install_ci/lib/coq)/ - - make -j ${NJOBS} BIN="$BIN" LIB="$LIB" all + - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all artifacts: name: "$CI_JOB_NAME.logs" when: on_failure @@ -163,151 +117,90 @@ before_script: script: - set -e - echo 'start:coq.test' - - make -f Makefile.ci -j ${NJOBS} ${TEST_TARGET} + - make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET} - echo 'end:coq.test' - set +e dependencies: - - opam-boot - build variables: &ci-template-vars TEST_TARGET: "$CI_JOB_NAME" - EXTRA_PACKAGES: "$TIMING_PACKAGES" - -opam-boot: - <<: *opam-boot-template - cache: - paths: &cache-paths - - .opamcache - key: "main-$CACHEKEY" - variables: - EXTRA_OPAM: "$COQIDE_OPAM ocamlgraph $ELPI_OPAM" - EXTRA_PACKAGES: "$COQIDE_PACKAGES" - -opam-boot:32bit: - <<: *opam-boot-template - cache: - paths: *cache-paths - key: "32bit-$CACHEKEY" - variables: - COMPILER: "$COMPILER_32BIT" - EXTRA_PACKAGES: "gcc-multilib" - -opam-boot:bleeding-edge: - <<: *opam-boot-template - cache: - paths: *cache-paths - key: "be-$CACHEKEY" - variables: - COMPILER: "$COMPILER_BLEEDING_EDGE" - CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" - EXTRA_PACKAGES: "$COQIDE_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM_BE" build: <<: *build-template - dependencies: - - opam-boot variables: EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" - EXTRA_PACKAGES: "$COQIDE_PACKAGES $COQDOC_PACKAGES" - PIP_PACKAGES: "$SPHINX_PACKAGES" # no coqide for 32bit: libgtk installation problems build:32bit: <<: *build-template - dependencies: - - opam-boot:32bit variables: + OPAM_VARIANT: "+32bit" EXTRA_CONF: "-native-compiler yes" - EXTRA_PACKAGES: "gcc-multilib" build:bleeding-edge: <<: *build-template - dependencies: - - opam-boot:bleeding-edge variables: + OPAM_SWITCH: be EXTRA_CONF: "-native-compiler yes -coqide opt" - EXTRA_PACKAGES: "$COQIDE_PACKAGES" warnings: <<: *warnings-template - dependencies: - - opam-boot # warnings:32bit: # <<: *warnings-template # variables: # <<: *warnings-variables -# EXTRA_PACKAGES: "$gcc-multilib COQIDE_PACKAGES_32BIT" -# dependencies: -# - opam-boot:32bit warnings:bleeding-edge: <<: *warnings-template - dependencies: - - opam-boot:bleeding-edge + variables: + OPAM_SWITCH: be test-suite: <<: *test-suite-template dependencies: - - opam-boot - build - variables: - EXTRA_PACKAGES: "$TIMING_PACKAGES" test-suite:32bit: <<: *test-suite-template dependencies: - - opam-boot:32bit - build:32bit variables: - EXTRA_PACKAGES: "gcc-multilib $TIMING_PACKAGES" + OPAM_VARIANT: "+32bit" test-suite:bleeding-edge: <<: *test-suite-template dependencies: - - opam-boot:bleeding-edge - build:bleeding-edge variables: - EXTRA_PACKAGES: "$TIMING_PACKAGES" + OPAM_SWITCH: be validate: <<: *validate-template dependencies: - - opam-boot - build validate:32bit: <<: *validate-template dependencies: - - opam-boot:32bit - build:32bit variables: - EXTRA_PACKAGES: "gcc-multilib" + OPAM_VARIANT: "+32bit" ci-bignums: <<: *ci-template ci-color: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES" ci-compcert: <<: *ci-template ci-coq-dpdgraph: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-coquelicot: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-elpi: <<: *ci-template @@ -315,10 +208,6 @@ ci-elpi: ci-equations: <<: *ci-template -ci-geocoq: - <<: *ci-template - allow_failure: true - ci-fcsl-pcm: <<: *ci-template @@ -329,24 +218,18 @@ ci-fcsl-pcm: ci-fiat-parsers: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES" ci-flocq: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-formal-topology: <<: *ci-template +ci-geocoq: + <<: *ci-template + ci-hott: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-iris-lambda-rust: <<: *ci-template @@ -368,9 +251,6 @@ ci-pidetop: ci-sf: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES wget" ci-unimath: <<: *ci-template diff --git a/.travis.yml b/.travis.yml index fce19f9d9..eeb0b800e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,11 +39,11 @@ env: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" - - COMPILER_BE="4.06.0" + - COMPILER_BE="4.06.1" - CAMLP5_VER=".6.14" - CAMLP5_VER_BE=".7.03" - FINDLIB_VER=".1.4.1" - - FINDLIB_VER_BE=".1.7.3" + - FINDLIB_VER_BE=".1.8.0" - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6" - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" @@ -67,7 +67,7 @@ matrix: - TEST_TARGET="ci-color" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-compcert" + - TEST_TARGET="ci-compcert" EXTRA_OPAM="menhir" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fbdeff20c..8d490591b 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")" CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" -opam install -j "$NJOBS" -y menhir git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}" ( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md new file mode 100644 index 000000000..8e677f6f2 --- /dev/null +++ b/dev/ci/docker/README.md @@ -0,0 +1,65 @@ +## Overall Docker Setup for Coq's CI. + +This directory provides Docker images to be used by Coq's CI. The +images do support Docker autobuild on `hub.docker.com` + +Autobuild is the preferred build method [see below]; if you are a +member of the `coqci` organization, the automated build will push the +image to the `coqci/name:$VERSION` tag using a Docker hub hook. + +## Updating the Image and Syncronization with CI files + +Unfortunately, at this point some manual synchronization is needed +between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the +checklist is: + +- check the name and version of the image setup in `hooks/post_push` + have to match. +- check `COMPILER` variables do match. + +Once you are sure the variables are right, then proceed to trigger an +autobuild or do a manual build, et voilà ! + +## Docker Autobuilding. + +We provide basic support for auto-building, see: + +https://docs.docker.com/docker-cloud/builds/advanced/ + +If you are member of the `coqci` Docker organization, trigger an +autobuild in your account and the image will be pushed to it as we +set the proper tag in `hooks/post_push`. + +We still need to figure out how properly setup a more automated, +organization-wide auto-building process. + +## Manual Building + +You can also manually build and push any image: + +- Build the image `docker build -t base:$VERSION .` + +To upload/push to your hub: + +- Create a https://hub.docker.com account. +- Login into your space `docker login --username=$USER` +- Push the image: + + `docker tag base:$VERSION $USER/base:$VERSION` + + `docker push $USER/base:$VERSION` + +Now your docker image is ready to be used. To upload to `coqci`: +- `docker tag base:$VERSION coqci/base:$VERSION` +- `docker push coqci/base:$VERSION` + +## Debugging / Misc + +To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>` + +Each `RUN` command creates an "layer", thus a Docker build is +incremental and it always help to put things updated more often at the +end. + +## Possible Improvements: + +- Use ARG for customizing versions, centralize variable setup; +- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry . diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile new file mode 100644 index 000000000..5698175c5 --- /dev/null +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -0,0 +1,45 @@ +FROM ubuntu:bionic +LABEL maintainer="e@x80.org" + +ENV DEBIAN_FRONTEND="noninteractive" + +RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \ + libgtk2.0-dev libgtksourceview2.0-dev \ + texlive-latex-extra texlive-fonts-recommended hevea \ + python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip + +RUN pip3 install antlr4-python3-runtime + +# Basic OPAM setup +ENV NJOBS="2" \ + OPAMROOT=/root/.opamcache \ + OPAMROOTISOK="true" + +ENV COMPILER="4.02.3" \ + BASE_OPAM="num ocamlfind jbuilder" + +RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update + +# Setup of the base switch +ENV CAMLP5_VER="6.14" \ + COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" \ + CI_OPAM="menhir elpi ocamlgraph" + +RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM + +# base+32bit switch +RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER + +# BE switch +ENV COMPILER_BE="4.06.1" \ + CAMLP5_VER_BE="7.05" \ + COQIDE_OPAM_BE="lablgtk.2.18.6 conf-gtksourceview.2" + +RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE + +# BE+flambda switch +RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push new file mode 100755 index 000000000..008ef1af3 --- /dev/null +++ b/dev/ci/docker/bionic_coq/hooks/post_push @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +COQCI_VERSION=V2018-05-05 +docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION +docker push $DOCKER_REPO:$COQCI_VERSION + +docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION +docker push coqci/base:$COQCI_VERSION |