ci-fiat_crypto: try setting -async-proofs-tac-j 0

SkySkimmer · Nov 20, 2023 · 8661cf8 · 8661cf8
1 parent b262feb
commit 8661cf8
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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 ||