Add color in the CI

We export a global "COQEXTRAFLAGS" in ci-wrapper.sh containing 'color yes'.
Villetaneuse · Nov 19, 2023 · dd4e976 · dd4e976
1 parent 257b88d
commit dd4e976
Show file tree

Hide file tree

Showing 17 changed files with 17 additions and 16 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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...'