buildjob

@@ -26,6 +26,11 @@ set -o pipefail
 . ci/prepare-opam.sh $OPAM_PINS # deliberately not quoted
 env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
 
+# maybe set some coq flags
+if [[ -n "$MANGLE_NAMES" ]]; then
+    export COQEXTRAFLAGS="$COQEXTRAFLAGS -mangle-names mangled_"
+fi
+
 # Build
 echo_color "$BOLDGREEN" "[buildjob] Perfoming build"
 time make --output-sync --no-print-directory -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt

prepare-opam.sh

@@ -40,7 +40,8 @@ test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-s
 echo
 
 # We really want to run all of the following in one opam transaction, but due to opam limitations,
-# that is not currently possible.
+# that is not currently possible.  Once we use opam 2 for CI, we can first do all the pinning (with `-n`)
+# followed by `opam upgrade --all build-dep/` (and hope this will also --fixup).
 
 # Install fixed versions of some dependencies.
 echo_color "$BOLDGREEN" "[prepare-opam] Processing pins"