diff options
| author | Emilio Jesus Gallego Arias | 2020-04-06 19:58:39 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-08 17:20:00 -0400 |
| commit | c7b82d512e15c857cf8176dfae9584fdf203fafa (patch) | |
| tree | 4ce0df198d153dde9c68e45235e29adb923c17b1 | |
| parent | 459faeddd095789affa30e7cf3b59fdaf95c1a0f (diff) | |
[ci] [fiat-crypto] [flambda] Don't use flambda for fiat-crypto
As of today flambda is pretty stack-hungry for some developments, in
particular it doesn't work [`StackOverflow` in fiat-crypto extracted
code even with large stacks.
We are thus forced to revert fiat-crypto's compilation to the regular
OCaml compiler.
This is OCaml bug https://github.com/ocaml/ocaml/issues/7842
| -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 |