diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 344 |
1 files changed, 205 insertions, 139 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f0d7463fc..06db0b7b7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,80 +1,80 @@ -image: ocaml/opam:ubuntu - -# this doesn't seem to work -cache: - paths: - - .opamcache +image: "$IMAGE" stages: + - docker - build - test +# some default values variables: - # some default values - NJOBS: "2" - COMPILER: "system" - CAMLP5_VER: "6.14" - - # some useful values - COMPILER_32BIT: "4.02.3+32bit" - - COMPILER_BLEEDING_EDGE: "4.06.0" - CAMLP5_VER_BLEEDING_EDGE: "7.03" - - TIMING_PACKAGES: "time python" - - COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" - #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" - COQIDE_OPAM: "lablgtk-extras" - COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6" - COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa python3-pip" - COQDOC_OPAM: "hevea" - SPHINX_PACKAGES: "bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex" - + # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here + # for reference] + CACHEKEY: "bionic_coq-V2018-06-04-V2" + IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" + # 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: "" + +docker-boot: + stage: docker + image: docker:stable + services: + - docker:dind + before_script: [] + script: + - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY" + - cd dev/ci/docker/bionic_coq/ + - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi + - docker build -t "$IMAGE" . + - docker push "$IMAGE" + except: + variables: + - $SKIP_DOCKER == "true" + tags: + - docker before_script: - - ls # figure out if artifacts are around - - printenv -# - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi - - if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -qq && sudo apt-get install -y -qq ${EXTRA_PACKAGES}; fi - - if [ -n "${PIP_PACKAGES}" ]; then sudo pip3 install ${PIP_PACKAGES}; fi - - # setup cache - - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi - - ln -s $(readlink -f .opamcache) ~/.opam - - # the default repo in this docker image is a local directory - # at the time of 4aaeb8abf it lagged behind the official - # repository such that camlp5 7.01 was not available - - opam repository set-url default https://opam.ocaml.org - - opam update - - opam switch ${COMPILER} + - cat /proc/{cpu,mem}info || true + - ls -a # figure out if artifacts are around + - printenv -0 | sort -z | tr '\0' '\n' + - declare -A switch_table + - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" ) + - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT" - eval $(opam config env) - - opam config list - - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM} - - rm -rf ~/.opam/log/ - opam list + - opam config list -# TODO figure out how to build doc for installed coq +################ GITLAB CACHING ###################### +# - use artifacts between jobs # +###################################################### + +# TODO figure out how to build doc for installed Coq .build-template: &build-template stage: build + retry: 1 artifacts: name: "$CI_JOB_NAME" paths: - _install_ci - config/Makefile + - config/coq_config.py - test-suite/misc/universes/all_stdlib.v expire_in: 1 week script: - set -e + - echo 'start:coq.clean' + - make clean # ensure that `make clean` works on a fresh clone + - echo 'end:coq.clean' + - echo 'start:coq.config' - - ./configure -prefix "$(pwd)/_install_ci" ${EXTRA_CONF} + - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" - echo 'end:coq.config' - echo 'start:coq.build' - - make -j ${NJOBS} byte - - make -j ${NJOBS} + - make -j "$NJOBS" byte + - make -j "$NJOBS" world $EXTRA_TARGET - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' @@ -89,41 +89,66 @@ before_script: .warnings-template: &warnings-template # keep warnings in test stage so we can test things even when warnings occur stage: test - dependencies: [] script: - set -e + - echo 'start:coq.clean' + - make clean # ensure that `make clean` works on a fresh clone + - echo 'end:coq.clean' + - echo 'start:coq.config' - - ./configure -local ${EXTRA_CONF} + - ./configure -local ${COQ_EXTRA_CONF} - 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" + COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes" + +# 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. +.doc-templare: &doc-template + stage: test + dependencies: + - not-a-real-job + script: + - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no' + - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx + - make install-doc-sphinx + artifacts: + name: "$CI_JOB_NAME" + paths: + - _install_ci/share/doc/coq/ + +# set dependencies when using .test-suite-template: &test-suite-template stage: test + dependencies: + - not-a-real-job script: - cd test-suite - make clean # 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 paths: - test-suite/logs +# set dependencies when using .validate-template: &validate-template stage: test + dependencies: + - not-a-real-job script: - cd _install_ci - find lib/coq/ -name '*.vo' -print0 > vofiles @@ -135,179 +160,220 @@ 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: - - build + - build:base variables: &ci-template-vars TEST_TARGET: "$CI_JOB_NAME" - EXTRA_PACKAGES: "$TIMING_PACKAGES" -build: +.ci-template-flambda: &ci-template-flambda + <<: *ci-template + dependencies: + - build:edge+flambda + variables: + <<: *ci-template-vars + OPAM_SWITCH: "edge" + OPAM_VARIANT: "+flambda" + +.windows-template: &windows-template + stage: test + artifacts: + name: "%CI_JOB_NAME%" + paths: + - dev\nsis\*.exe + - coq-opensource-archive-windows-*.zip + expire_in: 1 week + dependencies: [] + tags: + - windows + before_script: [] + script: + - call dev/ci/gitlab.bat + only: + variables: + - $WINDOWS == "enabled" + +build:base: <<: *build-template variables: - EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" - EXTRA_PACKAGES: "$COQIDE_PACKAGES $COQDOC_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM $COQDOC_OPAM" - PIP_PACKAGES: "$SPHINX_PACKAGES" + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" + # coqdoc for stdlib, until we know how to build it from installed Coq + EXTRA_TARGET: "stdlib" # no coqide for 32bit: libgtk installation problems -build:32bit: +build:base+32bit: + <<: *build-template + variables: + OPAM_VARIANT: "+32bit" + COQ_EXTRA_CONF: "-native-compiler yes" + +build:edge: <<: *build-template variables: - EXTRA_CONF: "-native-compiler yes" - EXTRA_PACKAGES: "gcc-multilib" - COMPILER: "$COMPILER_32BIT" + OPAM_SWITCH: edge + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" -build:bleeding-edge: +build:edge+flambda: <<: *build-template variables: - EXTRA_CONF: "-native-compiler yes -coqide opt" - COMPILER: "$COMPILER_BLEEDING_EDGE" - CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" - EXTRA_PACKAGES: "$COQIDE_PACKAGES" - EXTRA_OPAM: "$COQIDE_OPAM_BE" + OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" + COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts " + COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" -warnings: +windows64: + <<: *windows-template + variables: + ARCH: "64" + +windows32: + <<: *windows-template + variables: + ARCH: "32" + +warnings:base: <<: *warnings-template # warnings:32bit: # <<: *warnings-template # variables: # <<: *warnings-variables -# EXTRA_PACKAGES: "$gcc-multilib COQIDE_PACKAGES_32BIT" -# COMPILER: "$COMPILER_32BIT" -warnings:bleeding-edge: +warnings:edge: <<: *warnings-template variables: <<: *warnings-variables - COMPILER: "$COMPILER_BLEEDING_EDGE" - CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" - EXTRA_OPAM: "$COQIDE_OPAM_BE" + OPAM_SWITCH: edge + +documentation: + <<: *doc-template + dependencies: + - build:base + +test-suite:base: + <<: *test-suite-template + dependencies: + - build:base -test-suite: +test-suite:base+32bit: <<: *test-suite-template dependencies: - - build + - build:base+32bit variables: - EXTRA_PACKAGES: "$TIMING_PACKAGES" + OPAM_VARIANT: "+32bit" -test-suite:32bit: +test-suite:edge: <<: *test-suite-template dependencies: - - build:32bit + - build:edge variables: - COMPILER: "$COMPILER_32BIT" - EXTRA_PACKAGES: "gcc-multilib $TIMING_PACKAGES" + OPAM_SWITCH: edge -test-suite:bleeding-edge: +test-suite:edge+flambda: <<: *test-suite-template dependencies: - - build:bleeding-edge + - build:edge+flambda + variables: + OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" + +validate:base: + <<: *validate-template + dependencies: + - build:base + +validate:base+32bit: + <<: *validate-template + dependencies: + - build:base+32bit variables: - COMPILER: "$COMPILER_BLEEDING_EDGE" - CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE" - EXTRA_PACKAGES: "$TIMING_PACKAGES" + OPAM_VARIANT: "+32bit" -validate: +validate:edge: <<: *validate-template dependencies: - - build + - build:edge + variables: + OPAM_SWITCH: edge -validate:32bit: +validate:edge+flambda: <<: *validate-template dependencies: - - build:32bit + - build:edge+flambda variables: - COMPILER: "$COMPILER_32BIT" - EXTRA_PACKAGES: "gcc-multilib" + OPAM_SWITCH: edge + OPAM_VARIANT: "+flambda" ci-bignums: <<: *ci-template ci-color: - <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES" + <<: *ci-template-flambda ci-compcert: - <<: *ci-template + <<: *ci-template-flambda ci-coq-dpdgraph: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_OPAM: "ocamlgraph" - EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-coquelicot: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" + +ci-cross-crypto: + <<: *ci-template ci-elpi: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" ci-equations: <<: *ci-template -ci-geocoq: +ci-fcsl-pcm: <<: *ci-template - allow_failure: true -# ci-fiat-crypto: -# <<: *ci-template -# # out of memory error -# allow_failure: true +ci-fiat-crypto: + <<: *ci-template-flambda 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-template-flambda + +ci-geocoq: + <<: *ci-template-flambda ci-hott: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" ci-iris-lambda-rust: - <<: *ci-template + <<: *ci-template-flambda ci-ltac2: <<: *ci-template -ci-math-classes: +ci-math-comp: + <<: *ci-template-flambda + +ci-mtac2: <<: *ci-template -ci-math-comp: +ci-pidetop: <<: *ci-template +ci-quickchick: + <<: *ci-template-flambda + ci-sf: <<: *ci-template - variables: - <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES wget" ci-unimath: - <<: *ci-template + <<: *ci-template-flambda ci-vst: - <<: *ci-template + <<: *ci-template-flambda |