diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-09 15:24:01 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-09 15:24:01 +0200 |
| commit | 372737ba74baa2af8ee798df1b2768a5d827a179 (patch) | |
| tree | 3c81b58f6257abd797f2d015d467036537dd31a3 | |
| parent | e922afb970cee19a8421a6fa5f246c74a7ee8856 (diff) | |
| parent | 88650b2e689972d79ea2d9bfad03366f1fca01a4 (diff) | |
Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq.
| -rw-r--r-- | .gitlab-ci.yml | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1c4346bed..1789846c8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -125,6 +125,15 @@ before_script: variables: &ci-template-vars TEST_TARGET: "$CI_JOB_NAME" +.ci-template-flambda: &ci-template-flambda + <<: *ci-template + dependencies: + - build:edge+flambda + variables: + <<: *ci-template-vars + OPAM_SWITCH: "edge" + OPAM_VARIANT: "+flambda" + build:base: <<: *build-template variables: @@ -222,10 +231,10 @@ ci-bignums: <<: *ci-template ci-color: - <<: *ci-template + <<: *ci-template-flambda ci-compcert: - <<: *ci-template + <<: *ci-template-flambda ci-coq-dpdgraph: <<: *ci-template @@ -243,7 +252,7 @@ ci-fcsl-pcm: <<: *ci-template ci-fiat-crypto: - <<: *ci-template + <<: *ci-template-flambda ci-fiat-parsers: <<: *ci-template @@ -252,16 +261,16 @@ ci-flocq: <<: *ci-template ci-formal-topology: - <<: *ci-template + <<: *ci-template-flambda ci-geocoq: - <<: *ci-template + <<: *ci-template-flambda ci-hott: <<: *ci-template ci-iris-lambda-rust: - <<: *ci-template + <<: *ci-template-flambda ci-ltac2: <<: *ci-template @@ -270,7 +279,7 @@ ci-math-classes: <<: *ci-template ci-math-comp: - <<: *ci-template + <<: *ci-template-flambda ci-mtac2: <<: *ci-template @@ -282,7 +291,7 @@ ci-sf: <<: *ci-template ci-unimath: - <<: *ci-template + <<: *ci-template-flambda ci-vst: - <<: *ci-template + <<: *ci-template-flambda |