From 8661cf83246842a4911a412cf224f231645a1db8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 15 Nov 2023 09:50:30 +0100
Subject: [PATCH] ci-fiat_crypto: try setting -async-proofs-tac-j 0

---
 dev/ci/ci-fiat_crypto.sh | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 89b2bde870363..c1f6b8b3940ef 100644
--- a/dev/ci/ci-fiat_crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
@@ -18,8 +18,14 @@ stacksize=32768
 make_args=(EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1)
 
 export COQEXTRAFLAGS='-native-compiler no' # following bedrock2
+
 ( cd "${CI_BUILD_DIR}/fiat_crypto"
   ulimit -s $stacksize
+  if ! grep -q async-proofs-tac-j Makefile.coq.local; then
+    echo 'OTHERFLAGS += -async-proofs-tac-j 0' > tmp
+    cat Makefile.coq.local >> tmp
+    mv tmp Makefile.coq.local
+  fi
   make "${make_args[@]}" pre-standalone-extracted printlite lite ||
     make -j 1 "${make_args[@]}" pre-standalone-extracted printlite lite
   make "${make_args[@]}" all-except-compiled ||