diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-05 20:58:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 01:26:51 +0200 |
| commit | 88650b2e689972d79ea2d9bfad03366f1fca01a4 (patch) | |
| tree | 7d4166baa67438e468ab6bcf611e5b234f7e9aca /.gitlab-ci.yml | |
| parent | cde263581c49a75f8abdbcb398511942906e6204 (diff) | |
[gitlab] Do expensive builds with a flambda-compiled Coq.
Gains seem superior to 50%, but data is taken from Gitlab so no
reliable at all.
Diffstat (limited to '.gitlab-ci.yml')
| -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 |