16 files changed, 71 insertions, 58 deletions
diff --git a/dev/base_include b/dev/base_include
index 061bf1f3e1..b761924b46 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -68,7 +68,7 @@ open Constr_matching
 open Glob_term
 open Glob_ops
 open Coercion
-open Recordops
+open Structures
 open Detyping
 open Reductionops
 open Evarconv
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
deleted file mode 100755
index 2550cbb31c..0000000000
--- a/dev/build/osx/make-macos-dmg.sh
+++ /dev/null
@@ -1,37 +0,0 @@
-#!/bin/bash
-
-# Fail on first error
-set -e
-
-# Configuration setup
-DMGDIR=$PWD/_dmg
-VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
-APP=bin/CoqIDE_${VERSION}.app
-
-# Install Coq into the .app file
-make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources" install-coq install-ide-toploop
-
-# Fill .app file with metadata and other .app specific stuff (like non-system .so)
-make PRIVATEBINARIES="$APP" -j 1 -l2 "$APP" VERBOSE=1
-
-# Create the dmg bundle
-mkdir -p "$DMGDIR"
-ln -sf /Applications "$DMGDIR/Applications"
-cp -r "$APP" "$DMGDIR"
-
-mkdir -p _build
-
-# Temporary countermeasure to hdiutil error 5341
-# head -c9703424 /dev/urandom > $DMGDIR/.padding
-
-hdi_opts=(-volname "coq-$VERSION-installer-macos"
-          -srcfolder "$DMGDIR"
-          -ov # overwrite existing file
-          -format UDZO
-          -imagekey "zlib-level=9"
-
-          # needed for backward compat since macOS 10.14 which uses APFS by default
-          # see discussion in #11803
-          -fs hfs+
-         )
-hdiutil create "${hdi_opts[@]}" "_build/coq-$VERSION-installer-macos.dmg"
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 67555da0a2..0093b5fca2 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -139,7 +139,8 @@ project compcert "https://github.com/AbsInt/CompCert" "master"
 ########################################################################
 # VST
 ########################################################################
-project vst "https://github.com/PrincetonUniversity/VST" "master"
+# todo: 2021 03 11: switch back to master once vst merges the compcert3.9 branch
+project vst "https://github.com/PrincetonUniversity/VST" "compcert3.9"
 
 ########################################################################
 # cross-crypto
@@ -247,7 +248,7 @@ project reduction_effects "https://github.com/coq-community/reduction-effects" "
 # menhirlib
 ########################################################################
 # Note: menhirlib is now in subfolder coq-menhirlib of menhir
-project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20201122"
+project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20210310"
 
 ########################################################################
 # aac_tactics
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 006565df5c..6d1e6d788a 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -138,8 +138,8 @@ make()
     if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ];
     then
         # Not submake and parallel make requested
-        command make --output-sync -j "$NJOBS" "$@"
+        command make -j "$NJOBS" "$@"
     else
-        command make --output-sync "$@"
+        command make "$@"
     fi
 }
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index cb6c3e6452..01723e5b5c 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -5,4 +5,10 @@ ci_dir="$(dirname "$0")"
 
 git_download flocq
 
-( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
+( cd "${CI_BUILD_DIR}/flocq"
+  ( if [ ! -x ./configure ]; then
+      autoconf
+      ./configure COQEXTRAFLAGS="-compat 8.13";
+    fi )
+  ./remake "-j${NJOBS}"
+  ./remake install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8f14625c63..00729cd168 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -24,7 +24,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         texlive-science tipa
 
 # More dependencies of the sphinx doc, pytest for coqtail
-RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
+RUN pip3 install docutils==0.16 sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
         antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 \
         pytest==5.4.3
 
@@ -44,7 +44,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
     CI_OPAM="ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.13.0"
+    BASE_ONLY_OPAM="elpi.1.13.1"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
diff --git a/dev/ci/user-overlays/13958-gares-recordops-api.sh b/dev/ci/user-overlays/13958-gares-recordops-api.sh
new file mode 100644
index 0000000000..0ec50a1dda
--- /dev/null
+++ b/dev/ci/user-overlays/13958-gares-recordops-api.sh
@@ -0,0 +1,6 @@
+overlay metacoq https://github.com/gares/metacoq recordops-api 13958
+overlay mtac2 https://github.com/gares/Mtac2 recordops-api 13958
+overlay elpi https://github.com/gares/coq-elpi recordops-api 13958
+overlay unicoq https://github.com/gares/unicoq recordops-api 13958
+overlay equations https://github.com/gares/Coq-Equations recordops-api 13958
+overlay hierarchy_builder https://github.com/gares/hierarchy-builder coq-master 13958
diff --git a/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh
new file mode 100644
index 0000000000..d1606711dc
--- /dev/null
+++ b/dev/ci/user-overlays/14050-SkySkimmer-no-remote-counter-alt.sh
@@ -0,0 +1 @@
+overlay metacoq https://github.com/SkySkimmer/metacoq no-remote-counter-alt 14050
diff --git a/dev/ci/user-overlays/14111-gares-update-elpi.sh b/dev/ci/user-overlays/14111-gares-update-elpi.sh
new file mode 100644
index 0000000000..8827127a38
--- /dev/null
+++ b/dev/ci/user-overlays/14111-gares-update-elpi.sh
@@ -0,0 +1,2 @@
+overlay elpi https://github.com/LPCIC/coq-elpi coq-master+1.9.5 14111
+overlay hierarchy_builder https://github.com/math-comp/hierarchy-builder coq-master+1.1.0 14111
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
index da3022644d..db51dc08b6 100644
--- a/dev/core_dune.dbg
+++ b/dev/core_dune.dbg
@@ -6,7 +6,7 @@ load_printer clib.cma
 load_printer dynlink.cma
 load_printer lib.cma
 load_printer gramlib.cma
-load_printer byterun.cma
+load_printer coqrun.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index de3d5a3d15..8ebd6b5073 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -10,17 +10,23 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune).
 
 ## Quick Start
 
-Usually, using the latest version of Dune is recommended, see
-`dune-project` for the minimum required version; type `dune build` to
-build the base Coq libraries. No call to `./configure` is needed.
+Usually, using the latest version of Dune is recommended, see the
+first line of the `dune-project` file for the minimum required
+version.
+
+It is strongly recommended that you use the helper targets available
+in `Makefile.dune`, `make -f Makefile.dune` will display help. Note
+that dune will call configure for you if needed, so no need to call
+`./configure` in the regular development workflow.
+
+`dune build @install` will build all the public Coq artifacts; `dune
+build` will build all the targets in the workspace, including tests
+and documentations.
 
 Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
 the make-based system.
 
-More helper targets are available in `Makefile.dune`, `make -f
-Makefile.dune` will display some help.
-
 Dune places build artifacts in a separate directory `_build`; it will
 also generate an `.install` file so files can be properly installed by
 package managers.
@@ -84,7 +90,11 @@ builds, please see below.
 
 ## Documentation and testing targets
 
-Coq's test-suite can be run with `dune runtest`.
+Coq's test-suite can be run with `dune runtest`; given that `dune`
+still invokes the test-suite makefile, the environment variable
+`NJOBS` will control the value of the `-j` option that is passed to
+make; common call `NJOBS=8 dune runtest`. This will be resolved in the
+future once the test suite is ported to Dune rules.
 
 There is preliminary support to build the API documentation and
 reference manual in HTML format, use `dune build {@doc,@refman-html}`
@@ -229,3 +239,17 @@ useful to Coq, some examples are:
   implicitly loaded plugins / vo files. See the "Running binaries
   [coqtop / coqide]" section above as to how to correctly call Coq's
   binaries.
+
+## Dune cheat sheet
+
+- `dune build` build all targets in the current workspace
+- `dune build @check` build all ML targets as fast as possible, setup merlin
+- `dune utop $dir` open a shell for libraries in `$dir`
+- `dune exec -- $file` build and execute binary `$file`, can be in path or be an specific name
+- `dune build _build/$context/$foo` build target `$foo$` in `$context`, with build dir layout
+- `dune build _build/install/$context/foo` build target `$foo$` in `$context`, with install dir layout
+
+### packaging:
+
+- `dune subst` generate metadata for a package to be installed / distributed, necessary for opam
+- `dune build -p $pkg` build a package in release mode
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 4452baf513..5c8b8944a7 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -344,6 +344,16 @@ Conversion machines
         noticeable if activated by chance, since it usually breaks
         control-flow integrity
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: arbitrary code execution on irreducible PArray.set
+  introduced: 8.13
+  impacted released versions: 8.13.0, 8.13.1
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 8.13.2
+  found by: Melquiond
+  GH issue number: #13998
+  risk: none, unless using primitive array operations; systematic otherwise
+
 Side-effects
 
   component: side-effects
diff --git a/dev/dune b/dev/dune
index 9da06a3fab..d3ba5c7e3d 100644
--- a/dev/dune
+++ b/dev/dune
@@ -21,8 +21,8 @@
     %{lib:coq-core.clib:clib.cma}
     %{lib:coq-core.lib:lib.cma}
     %{lib:coq-core.kernel:kernel.cma}
-    %{lib:coq-core.vm:byterun.cma}
-    %{lib:coq-core.vm:../../stublibs/dllbyterun_stubs.so}
+    %{lib:coq-core.vm:coqrun.cma}
+    %{lib:coq-core.vm:../../stublibs/dllcoqrun_stubs.so}
     %{lib:coq-core.library:library.cma}
     %{lib:coq-core.engine:engine.cma}
     %{lib:coq-core.pretyping:pretyping.cma}
diff --git a/dev/dune_db_408 b/dev/dune_db_408
index bc86020d56..dff9b1e9e6 100644
--- a/dev/dune_db_408
+++ b/dev/dune_db_408
@@ -6,7 +6,7 @@ load_printer clib.cma
 load_printer dynlink.cma
 load_printer lib.cma
 load_printer gramlib.cma
-load_printer byterun.cma
+load_printer coqrun.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/dev/dune_db_409 b/dev/dune_db_409
index adb1f76872..6c9f701b65 100644
--- a/dev/dune_db_409
+++ b/dev/dune_db_409
@@ -5,7 +5,7 @@ load_printer config.cma
 load_printer clib.cma
 load_printer lib.cma
 load_printer gramlib.cma
-load_printer byterun.cma
+load_printer coqrun.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/dev/shim/dune b/dev/shim/dune
index e4cc7699f0..2c7f9c3fa9 100644
--- a/dev/shim/dune
+++ b/dev/shim/dune
@@ -26,7 +26,7 @@
  (targets coqbyte-prelude)
  (deps
   %{bin:coqtop.byte}
-  %{lib:coq-core.kernel:../../stublibs/dllbyterun_stubs.so}
+  %{lib:coq-core.kernel:../../stublibs/dllcoqrun_stubs.so}
   %{project_root}/theories/Init/Prelude.vo)
  (action
   (with-stdout-to %{targets}