diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index ba88e4cd5e6c6..728bc77529393 100644 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -10,7 +10,7 @@ git_download fiat_crypto if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/fiat_crypto/rupicola/bedrock2" COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make make install diff --git a/dev/ci/ci-category_theory.sh b/dev/ci/ci-category_theory.sh index b5ed059402559..9a4d299363db6 100644 --- a/dev/ci/ci-category_theory.sh +++ b/dev/ci/ci-category_theory.sh @@ -9,7 +9,7 @@ git_download category_theory if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/category_theory" make make install diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index e6ee79d5360e7..00962692406b8 100644 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -9,7 +9,7 @@ git_download color if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/color" make ) diff --git a/dev/ci/ci-coq_library_undecidability.sh b/dev/ci/ci-coq_library_undecidability.sh index 3ef55f97b46de..8564a562d64cf 100644 --- a/dev/ci/ci-coq_library_undecidability.sh +++ b/dev/ci/ci-coq_library_undecidability.sh @@ -9,7 +9,7 @@ git_download coq_library_undecidability if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/coq_library_undecidability" make make install diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 56b33a9ad7a6a..5226271603f35 100644 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -9,7 +9,7 @@ git_download corn if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/corn" ./configure.sh make diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh index d0134081b73ab..38eea71dbc4e3 100644 --- a/dev/ci/ci-engine_bench.sh +++ b/dev/ci/ci-engine_bench.sh @@ -9,7 +9,7 @@ git_download engine_bench if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler ondemand' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( 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 2df3462a8e425..e376c721b602b 100644 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -9,7 +9,7 @@ git_download equations if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/equations" [ -e Makefile.coq ] || ./configure.sh coq make diff --git a/dev/ci/ci-equations_test.sh b/dev/ci/ci-equations_test.sh index 2e7ae070ca1c9..0eb51116d541f 100644 --- a/dev/ci/ci-equations_test.sh +++ b/dev/ci/ci-equations_test.sh @@ -7,7 +7,7 @@ ci_dir="$(dirname "$0")" if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/equations" make test-suite examples ) diff --git a/dev/ci/ci-fiat_crypto.sh b/dev/ci/ci-fiat_crypto.sh index 89b2bde870363..93adc5f78cf5c 100644 --- a/dev/ci/ci-fiat_crypto.sh +++ b/dev/ci/ci-fiat_crypto.sh @@ -17,7 +17,7 @@ stacksize=32768 # version of other developments make_args=(EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1) -export COQEXTRAFLAGS='-native-compiler no' # following bedrock2 +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" # following bedrock2 ( cd "${CI_BUILD_DIR}/fiat_crypto" ulimit -s $stacksize make "${make_args[@]}" pre-standalone-extracted printlite lite || diff --git a/dev/ci/ci-fiat_crypto_legacy.sh b/dev/ci/ci-fiat_crypto_legacy.sh index 443d46e434f57..044b5b081501b 100644 --- a/dev/ci/ci-fiat_crypto_legacy.sh +++ b/dev/ci/ci-fiat_crypto_legacy.sh @@ -24,7 +24,7 @@ targets2=( selected-specific-display ) -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" make "${targets1[@]}" make -j 1 "${targets2[@]}" diff --git a/dev/ci/ci-jasmin.sh b/dev/ci/ci-jasmin.sh index 7f7f3f26dbad3..02c1722b517b2 100644 --- a/dev/ci/ci-jasmin.sh +++ b/dev/ci/ci-jasmin.sh @@ -9,7 +9,7 @@ git_download jasmin if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/jasmin" make -C proofs diff --git a/dev/ci/ci-lean_importer.sh b/dev/ci/ci-lean_importer.sh index c16ee489d6dec..0f87c2b47c456 100644 --- a/dev/ci/ci-lean_importer.sh +++ b/dev/ci/ci-lean_importer.sh @@ -9,7 +9,7 @@ git_download lean_importer if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/lean_importer" make diff --git a/dev/ci/ci-ltac2_compiler.sh b/dev/ci/ci-ltac2_compiler.sh index 49bc10d2939ec..9e6c70e6f6e3d 100644 --- a/dev/ci/ci-ltac2_compiler.sh +++ b/dev/ci/ci-ltac2_compiler.sh @@ -9,7 +9,7 @@ git_download ltac2_compiler if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/ltac2_compiler" make .merlin diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 6a4d958061d07..87cccb7f40ff0 100644 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -9,7 +9,7 @@ git_download metacoq if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/metacoq" [ -e pcuic/metacoq-config ] || ./configure.sh local make all TIMED=pretty-timed diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index ccd27b08b9f14..384ed12c6518f 100644 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -9,7 +9,7 @@ git_download unimath if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/unimath" # these files consumes too much memory for the shared workers # (at least with -j 2 when the scheduler runs them in parallel) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 14afef3d84558..eae339234b101 100644 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -15,7 +15,7 @@ if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi # export COMPCERT=bundled # See ci-compcert.sh -export COQEXTRAFLAGS='-native-compiler no' +COQEXTRAFLAGS="$COQEXTRAFLAGS -native-compiler no" ( cd "${CI_BUILD_DIR}/vst" make IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true ) diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh index 654475338d66b..4eb84a78e14ff 100755 --- a/dev/ci/ci-wrapper.sh +++ b/dev/ci/ci-wrapper.sh @@ -14,6 +14,7 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" cd "${DIR}/../.." || exit 1 export TIMED=1 +export COQEXTRAFLAGS='-color yes' bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log code=$? echo 'Aggregating timing log...'