9 files changed, 18 insertions, 48 deletions
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/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh
index 1b2d6a73a2..d2e0ee89bf 100755
--- a/dev/ci/ci-paramcoq.sh
+++ b/dev/ci/ci-paramcoq.sh
@@ -5,7 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download paramcoq
 
-# Typically flaky on our worker configuration
-# https://gitlab.com/coq/coq/-/jobs/1144081161
-export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples)
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/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/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}