diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 86 |
1 files changed, 75 insertions, 11 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 799f5b14..b936401a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,12 +9,13 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-v8.8-V2018-09-20" + CACHEKEY: "bionic_coq-v8.9-V2018-10-22" 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: "" + GIT_DEPTH: "10" docker-boot: stage: docker @@ -37,11 +38,11 @@ docker-boot: before_script: - cat /proc/{cpu,mem}info || true - ls -a # figure out if artifacts are around - - printenv | sort + - 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 switch set -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT" + - eval $(opam env) - opam list - opam config list @@ -60,23 +61,28 @@ after_script: 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 -warn-error yes -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" world $EXTRA_TARGET - make test-suite/misc/universes/all_stdlib.v - echo 'end:coq:build' - echo 'start:coq.install' - - make install + - make install install-byte $EXTRA_INSTALL - make install-byte - cp bin/fake_ide _install_ci/bin/ - echo 'end:coq.install' @@ -88,6 +94,19 @@ after_script: # purpose, we add a spurious dependency `not-a-real-job` that must be # overridden otherwise the CI will fail. +.doc-template: &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= refman + - 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 @@ -155,12 +174,15 @@ after_script: - call dev/ci/gitlab.bat only: variables: - - $WINDOWS == "enabled" + - $WINDOWS =~ /enabled/ build:base: <<: *build-template variables: - COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes" + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" + # coqdoc for stdlib, until we know how to build it from installed Coq + EXTRA_TARGET: "stdlib" + EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable" # no coqide for 32bit: libgtk installation problems build:base+32bit: @@ -225,6 +247,42 @@ pkg:nix: paths: - nix-build-coq.drv-0/*/test-suite/logs +build:macOS: + stage: build + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build + expire_in: 1 week + tags: + - macOS + dependencies: [] + before_script: [] + script: + - dev/build/osx/make-macos-dmg.sh + variables: + NJOBS: "2" + only: + variables: + - $MACOS == "enabled" + +doc:refman: + <<: *doc-template + dependencies: + - build:base + +doc:ml-api: + stage: test + dependencies: + - build:edge + script: + - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" + - make mli-doc source-doc # ml-doc [broken in 4.07.0] + artifacts: + name: "$CI_JOB_NAME" + paths: + - dev/ocamldoc + test-suite:base: <<: *test-suite-template dependencies: @@ -297,6 +355,9 @@ ci-coq-dpdgraph: ci-coquelicot: <<: *ci-template +ci-cross-crypto: + <<: *ci-template + ci-elpi: <<: *ci-template @@ -336,12 +397,15 @@ ci-ltac2: ci-math-comp: <<: *ci-template-flambda -ci-quickchick: - <<: *ci-template-flambda - ci-mtac2: <<: *ci-template +ci-pidetop: + <<: *ci-template + +ci-quickchick: + <<: *ci-template-flambda + ci-sf: <<: *ci-template |