23 files changed, 55 insertions, 2 deletions
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index d2e150be9a..7796ae3b01 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -52,7 +52,7 @@ check_variable "CI_JOB_URL"
 : "${new_coq_opam_archive_git_branch:=master}"
 : "${old_coq_opam_archive_git_branch:=master}"
 : "${num_of_iterations:=1}"
-: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast}"
+: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial}"
 
 new_coq_commit=$(git rev-parse HEAD^2)
 old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit)
@@ -269,6 +269,9 @@ create_opam() {
     opam repo add -q --this-switch coq-extra-dev "$OPAM_COQ_DIR/extra-dev"
     opam repo add -q --this-switch coq-released "$OPAM_COQ_DIR/released"
 
+    # Pinning for packages that are not in a repository
+    opam pin add -ynq coq-perennial.dev git+https://github.com/mit-pdos/perennial#coq/tested
+
     opam install -qy -j$number_of_processors $initial_opam_packages
     if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi
 
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 )
diff --git a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh
new file mode 100644
index 0000000000..95f0de2bd3
--- /dev/null
+++ b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "13386" ] || [ "$CI_BRANCH" = "master+fix9971-primproj-canonical-structure-on-evar-type" ]; then
+
+    unicoq_CI_REF=master+adapting-coq-pr13386
+    unicoq_CI_GITURL=https://github.com/herbelin/unicoq
+
+    elpi_CI_REF=coq-master+adapting-coq-pr13386
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 37619833ac..79c2155823 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -312,6 +312,26 @@ Conversion machines
   risk: none without using -allow-sprop (off by default in 8.10.0),
         otherwise could be exploited by mistake
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: buffer overflow on large accumulators
+  introduced: 8.1
+  impacted released versions: 8.1-8.12.1
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 8.13.0
+  found by: Dolan, Roux, Melquiond
+  GH issue number: ocaml/ocaml#6385, #11170
+  risk: medium, as it can happen for large irreducible applications
+
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: buffer overflow on large records and closures
+  introduced: 8.1
+  impacted released versions: 8.1-now
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in:
+  found by: Dolan, Roux, Melquiond
+  GH issue number: ocaml/ocaml#6385, #11170
+  risk: unlikely to be activated by chance, might happen for autogenerated code
+
 Side-effects
 
   component: side-effects
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 21d6fbe9aa..bfc186c862 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -46,6 +46,7 @@ install_printer Top_printers.pp_idpred
 install_printer Top_printers.pp_cpred
 install_printer Top_printers.pp_transparent_state
 install_printer Top_printers.pp_stack_t
+install_printer Top_printers.pp_estack_t
 install_printer Top_printers.pp_state_t
 install_printer Top_printers.ppmetas
 install_printer Top_printers.ppevm
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e4dd7ef52c..a9438c4aca 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -165,6 +165,7 @@ let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
 let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n)
+let pp_estack_t n = pp (Reductionops.Stack.pr pr_econstr n)
 let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
 
 (* proof printers *)
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 712f66112c..50495dc0a4 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -108,6 +108,7 @@ val pp_cpred : Names.Cpred.t -> unit
 val pp_transparent_state : TransparentState.t -> unit
 
 val pp_stack_t : Constr.t Reductionops.Stack.t -> unit
+val pp_estack_t : EConstr.t Reductionops.Stack.t -> unit
 val pp_state_t : Reductionops.state -> unit
 
 val ppmetas : Evd.Metaset.t -> unit