From d57ba6cdf28375fa638d813fc2a3f0b072721dad Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 24 Aug 2018 00:09:13 -0400
Subject: [ci-fiat-crypto] Build c-files

This tests the outputs of extraction, to some extent.
---
 dev/ci/ci-fiat-crypto.sh | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 659511dbea..c6d2f0cfd9 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,4 +9,7 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt
 
 ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
 
-( cd "${fiat_crypto_CI_DIR}" && make new-pipeline )
+# We need a larger stack size to not overflow ocamlopt+flambda when
+# building the executables.
+# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+( cd "${fiat_crypto_CI_DIR}" && ulimit -s 32768 && make new-pipeline c-files )
-- 
cgit v1.2.3