diff options
| -rw-r--r-- | .gitlab-ci.yml | 108 |
1 files changed, 88 insertions, 20 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7c9a5c9a31..ce0c1d9af7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -2,10 +2,15 @@ image: "$IMAGE" stages: - docker - - build - - test + - stage-1 # No dependencies + - stage-2 # Only dependencies in stage 1 + - stage-3 # Only dependencies in stage 1 and 2 + - stage-4 # Only dependencies in stage 1, 2 and 3 - deploy +# When a job has no dependencies, it goes to stage 1. +# Otherwise, we set "needs" and "dependencies" to the same value. + # some default values variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here @@ -53,7 +58,7 @@ before_script: # TODO figure out how to build doc for installed Coq .build-template: - stage: build + stage: stage-1 artifacts: name: "$CI_JOB_NAME" paths: @@ -91,7 +96,7 @@ before_script: # Template for building Coq + stdlib, typical use: overload the switch .dune-template: - stage: build + stage: stage-1 dependencies: [] script: - set -e @@ -107,7 +112,9 @@ before_script: expire_in: 1 week .dune-ci-template: - stage: test + stage: stage-2 + needs: + - build:edge+flambda:dune:dev dependencies: - build:edge+flambda:dune:dev script: @@ -129,7 +136,7 @@ before_script: # overridden otherwise the CI will fail. .doc-template: - stage: test + stage: stage-2 dependencies: - not-a-real-job script: @@ -144,7 +151,7 @@ before_script: # set dependencies when using .test-suite-template: - stage: test + stage: stage-2 dependencies: - not-a-real-job script: @@ -167,7 +174,7 @@ before_script: # set dependencies when using .validate-template: - stage: test + stage: stage-2 dependencies: - not-a-real-job script: @@ -183,18 +190,22 @@ before_script: expire_in: 2 months .ci-template: - stage: test + stage: stage-2 script: - set -e - echo 'start:coq.test' - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}" - echo 'end:coq.test' - set +e + needs: + - build:base dependencies: - build:base .ci-template-flambda: extends: .ci-template + needs: + - build:edge+flambda dependencies: - build:edge+flambda variables: @@ -202,7 +213,7 @@ before_script: OPAM_VARIANT: "+flambda" .windows-template: - stage: test + stage: stage-1 artifacts: name: "%CI_JOB_NAME%" paths: @@ -261,7 +272,7 @@ build:edge+flambda:dune:dev: build:base+async: extends: .build-template - stage: test + stage: stage-1 variables: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt" COQUSERFLAGS: "-async-proofs on" @@ -295,7 +306,7 @@ windows32: - /^pr-.*$/ lint: - stage: test + stage: stage-1 script: dev/lint-repository.sh dependencies: [] variables: @@ -303,7 +314,7 @@ lint: OPAM_SWITCH: base pkg:opam: - stage: test + stage: stage-1 # OPAM will build out-of-tree so no point in importing artifacts dependencies: [] script: @@ -320,7 +331,7 @@ pkg:opam: .nix-template: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git - stage: test + stage: stage-1 variables: # By default we use coq.cachix.org as an extra substituter but this can be overridden EXTRA_SUBSTITUTERS: https://coq.cachix.org @@ -367,7 +378,8 @@ pkg:nix:deploy:channel: only: variables: - $CACHIX_DEPLOYMENT_KEY - dependencies: + dependencies: [] + needs: - pkg:nix:deploy script: - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null @@ -385,6 +397,8 @@ doc:refman: extends: .doc-template dependencies: - build:base + needs: + - build:base doc:refman:dune: extends: .dune-ci-template @@ -414,6 +428,10 @@ doc:refman:deploy: - doc:ml-api:odoc - doc:refman:dune - doc:stdlib:dune + needs: + - doc:ml-api:odoc + - doc:refman:dune + - doc:stdlib:dune script: - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null - git clone git@github.com:coq/doc.git _deploy @@ -441,11 +459,15 @@ test-suite:base: extends: .test-suite-template dependencies: - build:base + needs: + - build:base test-suite:base+32bit: extends: .test-suite-template dependencies: - build:base+32bit + needs: + - build:base+32bit variables: OPAM_VARIANT: "+32bit" only: *full-ci @@ -454,15 +476,19 @@ test-suite:edge+flambda: extends: .test-suite-template dependencies: - build:edge+flambda + needs: + - build:edge+flambda variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" only: *full-ci test-suite:egde:dune:dev: - stage: test + stage: stage-2 dependencies: - build:edge+flambda:dune:dev + needs: + - build:edge+flambda:dune:dev script: make -f Makefile.dune test-suite variables: OPAM_SWITCH: edge @@ -476,7 +502,7 @@ test-suite:egde:dune:dev: # expire_in: never test-suite:edge+trunk+make: - stage: test + stage: stage-1 dependencies: [] script: - opam switch create 4.09.0 --empty @@ -503,7 +529,7 @@ test-suite:edge+trunk+make: only: *full-ci test-suite:edge+trunk+dune: - stage: test + stage: stage-1 dependencies: [] script: - opam switch create 4.09.0 --empty @@ -535,6 +561,8 @@ test-suite:base+async: extends: .test-suite-template dependencies: - build:base + needs: + - build:base variables: COQFLAGS: "-async-proofs on -async-proofs-cache force" timeout: "timeout 100m" @@ -547,11 +575,15 @@ validate:base: extends: .validate-template dependencies: - build:base + needs: + - build:base validate:base+32bit: extends: .validate-template dependencies: - build:base+32bit + needs: + - build:base+32bit variables: OPAM_VARIANT: "+32bit" only: *full-ci @@ -560,6 +592,8 @@ validate:edge+flambda: extends: .validate-template dependencies: - build:edge+flambda + needs: + - build:edge+flambda variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" @@ -569,6 +603,8 @@ validate:quick: extends: .validate-template dependencies: - build:quick + needs: + - build:quick only: variables: - $UNRELIABLE =~ /enabled/ @@ -584,6 +620,13 @@ library:ci-bedrock2: library:ci-color: extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - plugin:ci-bignums + dependencies: + - build:edge+flambda + - plugin:ci-bignums library:ci-compcert: extends: .ci-template-flambda @@ -608,6 +651,13 @@ library:ci-flocq: library:ci-corn: extends: .ci-template-flambda + stage: stage-4 + needs: + - build:edge+flambda + - library:ci-math-classes + dependencies: + - build:edge+flambda + - library:ci-math-classes library:ci-geocoq: extends: .ci-template-flambda @@ -618,6 +668,20 @@ library:ci-hott: library:ci-iris-lambda-rust: extends: .ci-template-flambda +library:ci-math-classes: + extends: .ci-template-flambda + stage: stage-3 + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci + needs: + - build:edge+flambda + - plugin:ci-bignums + dependencies: + - build:edge+flambda + - plugin:ci-bignums + library:ci-math-comp: extends: .ci-template-flambda @@ -642,7 +706,11 @@ plugin:ci-aac_tactics: extends: .ci-template plugin:ci-bignums: - extends: .ci-template + extends: .ci-template-flambda + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build_ci plugin:ci-coq_dpdgraph: extends: .ci-template @@ -666,7 +734,7 @@ plugin:ci-paramcoq: extends: .ci-template plugin:plugin-tutorial: - stage: test + stage: stage-1 dependencies: [] script: - ./configure -local -warn-error yes |