[CI] Deactivate native-compiler in some jobs

A few libraries in the CI don't compile with it
(out of memory).

17 files changed, 19 insertions, 1 deletions

diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 8570c34194..524555b69c 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download bedrock2
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make && make install )
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index a0094b1006..72fc613c43 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download color
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/color" && make )
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 9cb7a65ab5..6b09726606 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,6 +5,7 @@ ci_dir="$(dirname "$0")"
 
 git_download compcert
 
+export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert" && \
       ./configure -ignore-coq-version x86_32-linux && \
       make && \
diff --git a/dev/ci/ci-coqprime.sh b/dev/ci/ci-coqprime.sh
index a4fd296896..e12c36e6a7 100755
--- a/dev/ci/ci-coqprime.sh
+++ b/dev/ci/ci-coqprime.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download coqprime
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/coqprime" && make && make install)
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
index ac3978dc8d..785ff4c2ad 100755
--- a/dev/ci/ci-corn.sh
+++ b/dev/ci/ci-corn.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download corn
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh
index fda7649f88..d976356dd4 100755
--- a/dev/ci/ci-engine_bench.sh
+++ b/dev/ci/ci-engine_bench.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download engine_bench
 
+export COQEXTRAFLAGS='-native-compiler ondemand'
 ( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 30047e624b..3eda7161c1 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 3ecdb32a51..e8fa8c0be4 100755
--- a/dev/ci/ci-fiat_crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
@@ -18,6 +18,7 @@ fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} pre-standalone-extracted printlite lite"
 fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all-except-compiled"
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
         ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
         make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat_crypto_legacy.sh b/dev/ci/ci-fiat_crypto_legacy.sh
index 6d0a803401..57cc121bb4 100755
--- a/dev/ci/ci-fiat_crypto_legacy.sh
+++ b/dev/ci/ci-fiat_crypto_legacy.sh
@@ -9,5 +9,6 @@ git_download fiat_crypto_legacy
 fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded"
 fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display selected-specific selected-specific-display"
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
   make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} )
diff --git a/dev/ci/ci-fiat_crypto_ocaml.sh b/dev/ci/ci-fiat_crypto_ocaml.sh
index 20d3deb14f..c63690d5c9 100755
--- a/dev/ci/ci-fiat_crypto_ocaml.sh
+++ b/dev/ci/ci-fiat_crypto_ocaml.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && make ${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml lite-generated-files )
diff --git a/dev/ci/ci-fiat_parsers.sh b/dev/ci/ci-fiat_parsers.sh
index ac74ebf667..8409e25bdc 100755
--- a/dev/ci/ci-fiat_parsers.sh
+++ b/dev/ci/ci-fiat_parsers.sh
@@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download fiat_parsers
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 4b92c8cb4d..679bef3b5e 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")"
 
 git_download hott
 
-( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure && make && make validate )
+( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure \
+      && sed -i.bak 's/\(HOQC =.*\)/\1 -native-compiler no/' Makefile \
+      && make && make validate )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index 27876d68de..813ea9b07a 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download metacoq
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make .merlin && make ci-local && make install )
diff --git a/dev/ci/ci-perennial.sh b/dev/ci/ci-perennial.sh
index 306cbdf63c..43add8254a 100755
--- a/dev/ci/ci-perennial.sh
+++ b/dev/ci/ci-perennial.sh
@@ -6,4 +6,5 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download perennial
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/perennial" && git submodule update --init --recursive && make TIMED=false lite )
diff --git a/dev/ci/ci-rewriter.sh b/dev/ci/ci-rewriter.sh
index 235482ffeb..ec7ac5bddc 100755
--- a/dev/ci/ci-rewriter.sh
+++ b/dev/ci/ci-rewriter.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download rewriter
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/rewriter" && make && make install)
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 704e278a4b..3d320617f2 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -5,4 +5,5 @@ ci_dir="$(dirname "$0")"
 
 git_download unimath
 
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/unimath" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 4a332406a2..a151cf0ba6 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -7,4 +7,5 @@ git_download vst
 
 export COMPCERT=bundled
 
+sed -i.bak 's/\(COQC=.*\)/\1 -native-compiler no/' ${CI_BUILD_DIR}/vst/Makefile
 ( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true )