diff options
| author | Gaëtan Gilbert | 2020-04-10 10:14:48 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-10 10:14:48 +0200 |
| commit | e34cae33d494f4ad1a4a27c94a323a160dc67d9f (patch) | |
| tree | 8f01c3c58dea3e2ea13764aaac215c83f51fcf8b | |
| parent | 795df4b7a194b53b592ed327d2318ef5abc7d131 (diff) | |
| parent | c7b82d512e15c857cf8176dfae9584fdf203fafa (diff) | |
Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-crypto
Reviewed-by: SkySkimmer
| -rw-r--r-- | .gitlab-ci.yml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index caed21f5c3..acbec54695 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -105,6 +105,7 @@ before_script: script: # flambda can be pretty stack hungry, specially with -O3 # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244 + # and https://github.com/coq/coq/pull/11916#issuecomment-609977375 - ulimit -s 16384 - set -e - make -f Makefile.dune world @@ -667,8 +668,11 @@ library:ci-cross-crypto: library:ci-fcsl-pcm: extends: .ci-template +# We cannot use flambda due to +# https://github.com/ocaml/ocaml/issues/7842, see +# https://github.com/coq/coq/pull/11916#issuecomment-609977375 library:ci-fiat-crypto: - extends: .ci-template-flambda + extends: .ci-template stage: stage-4 needs: - build:edge+flambda |