From c7b82d512e15c857cf8176dfae9584fdf203fafa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 6 Apr 2020 19:58:39 -0400
Subject: [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
---
 .gitlab-ci.yml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3