19 files changed, 231 insertions, 23 deletions

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index c75acb0560..577ce35aae 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -420,6 +420,7 @@ copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOT
 ECHO ========== BUILD COQ ==========

 

 MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"

+RMDIR /S /Q "%CYGWIN_INSTALLDIR_WFMT%\build\patches"

 MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\patches"

 

 COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index f04de0ce6c..7342bc72e7 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -97,8 +97,11 @@
 ########################################################################
 # Coquelicot
 ########################################################################
-: "${coquelicot_CI_REF:=master}"
-: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
+# Modified until https://gitlab.inria.fr/coquelicot/coquelicot/merge_requests/2 is merged
+: "${coquelicot_CI_REF:=fix-rlist-import}"
+: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/pedrot/coquelicot}"
+# : "${coquelicot_CI_REF:=master}"
+# : "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
 : "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
 
 ########################################################################
@@ -256,6 +259,13 @@
 : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}"
 
 ########################################################################
+# reduction-effects
+########################################################################
+: "${reduction_effects_CI_REF:=master}"
+: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}"
+: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}"
+
+########################################################################
 # menhirlib
 ########################################################################
 : "${menhirlib_CI_REF:=master}"
diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh
index 2af4b58201..9ce5da9f50 100755
--- a/dev/ci/ci-fiat-crypto-legacy.sh
+++ b/dev/ci/ci-fiat-crypto-legacy.sh
@@ -6,8 +6,8 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download fiat_crypto_legacy
 
-fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display"
-fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+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"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \
   ./etc/ci/remove_autogenerated.sh && \
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 000c418137..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,11 +9,15 @@ git_download fiat_crypto
 # We need a larger stack size to not overflow ocamlopt+flambda when
 # building the executables.
 # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
+fiat_crypto_CI_STACKSIZE=32768
 
-fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1"
+# fiat-crypto is not guaranteed to build with the latest version of
+# bedrock2, so we use the pinned version of bedrock2, but the external
+# version of other developments
+fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1"
 fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite"
 fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all"
 
 ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
-        ulimit -s 32768 && \
+        ulimit -s ${fiat_crypto_CI_STACKSIZE} && \
         make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-reduction_effects.sh b/dev/ci/ci-reduction_effects.sh
new file mode 100755
index 0000000000..6b6de3fa2f
--- /dev/null
+++ b/dev/ci/ci-reduction_effects.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download reduction_effects
+
+( cd "${CI_BUILD_DIR}/reduction_effects" && make && make test && make install)
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 2b1d2298f2..b9d6215e60 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -4,7 +4,10 @@ ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
 CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
-data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
+
+# "latest" is disabled due to lack of build credits upstream, thus artifacts fail
+# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
+data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
 
 mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
 
diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
new file mode 100644
index 0000000000..a125337dd9
--- /dev/null
+++ b/dev/ci/user-overlays/11368-trailing-implicit-error.sh
@@ -0,0 +1,33 @@
+if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then
+
+    mathcomp_CI_REF=non_maximal_implicit
+    mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp
+
+    oddorder_CI_REF=non_maximal_implicit
+    oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order
+
+    stdlib2_CI_REF=non_maximal_implicit
+    stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2
+
+    coq_dpdgraph_CI_REF=non_maximal_implicit
+    coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph
+
+    vst_CI_REF=non_maximal_implicit
+    vst_CI_GITURL=https://github.com/SimonBoulier/VST
+
+    equations_CI_REF=non_maximal_implicit
+    equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations
+
+    mtac2_CI_REF=non_maximal_implicit
+    mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2
+
+    relation_algebra_CI_REF=non_maximal_implicit
+    relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra
+
+    fiat_parsers_CI_REF=non_maximal_implicit
+    fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat
+
+    Corn_CI_REF=non_maximal_implicit
+    Corn_CI_GITURL=https://github.com/SimonBoulier/corn
+
+fi
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 37c6e2f619..cd35064b18 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -108,24 +108,44 @@ automatically.
 You can use `ocamldebug` with Dune; after a build, do:
 
 ```
-dune exec -- dev/dune-dbg /path/to/foo.v
+dune exec -- dev/dune-dbg coqc foo.v
 (ocd) source dune_db
 ```
 
-or
+to start `coqc.byte foo.v`, other targets are `{checker,coqide,coqtop}`:
 
 ```
-dune exec -- dev/dune-dbg checker Foo
+dune exec -- dev/dune-dbg checker foo.vo
 (ocd) source dune_db
 ```
 
-for the checker. Unfortunately, dependency handling here is not fully
-refined, so you need to build enough of Coq once to use this target
-[it will then correctly compute the deps and rebuild if you call the
-script again] This will be fixed in the future.
+Unfortunately, dependency handling here is not fully refined, so you
+need to build enough of Coq once to use this target [it will then
+correctly compute the deps and rebuild if you call the script again]
+This will be fixed in the future.
 
 For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`.
 
+**Note**: If you are using OCaml >= 4.08 you need to use
+
+```
+(ocd) source dune_db_408
+```
+
+or
+
+```
+(ocd) source dune_db_409
+```
+
+depending on your OCaml version. This is due to several factors:
+
+- OCaml >= 4.08 doesn't allow doubly-linking modules, however `source`
+  is not re entrant and seems to doubly-load in the default setup, see
+  https://github.com/coq/coq/issues/8952
+- OCaml >= 4.09 comes with `dynlink` already linked in so we need to
+  modify the list of modules loaded.
+
 ## Dropping from coqtop:
 
 After doing `make -f Makefile.dune voboot`, the following commands should work:
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 04b20c6889..3bc92e6aee 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,13 @@
 
 ### ML API
 
+Exception handling:
+
+- Coq's custom `Backtrace` module has been removed in favor of OCaml's
+  native backtrace implementation. Please use the functions in
+  `Exninfo.capture` and `iraise` when re-raising inside an exception
+  handler.
+
 Printers:
 
 - Functions such as Printer.pr_lconstr_goal_style_env have been
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 2d187f7bae..3260040248 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -158,7 +158,7 @@ Universes
   component: universe polymorphism, asynchronous proofs
   summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
   introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
-  impacted released: V8.5-V8.10
+  impacted released versions: V8.5-V8.10
   impacted development branches: none
   impacted coqchk versions: immune
   fixed in: PR#10664
@@ -167,6 +167,19 @@ Universes
   GH issue number: none
   risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
 
+  component: algebraic universes
+  summary: Set+2 was incorrectly simplified to Set+1
+  introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a)
+  impacted released versions: V8.10.0 V8.10.1 V8.10.2
+  impacted coqchk versions: same
+  fixed in: PR#11422
+  found by: Gilbert
+  exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration)
+  GH issue number: see PR
+  risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic
+    universes such that +2 increments do not appear), mild risk from plugins which manipulate
+    algebraic universes.
+
 Primitive projections
 
   component: primitive projections, guard condition
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 1c486b024d..ba68501e04 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -75,7 +75,8 @@ in time.
 - [ ] Pin the versions of libraries and plugins in
   `dev/ci/ci-basic-overlays.sh` to use commit hashes or tag (or, if it
   exists, a branch dedicated to compatibility with the corresponding
-  Coq branch).
+  Coq branch). You can use the `dev/tools/pin-ci.sh` script to do this
+  semi-automatically.
 - [ ] Remove all remaining unmerged feature PRs from the beta milestone.
 - [ ] Start a new project to track PR backporting. The project should
   have a "Request X.X+beta1 inclusion" column for the PRs that were
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 0fc0a413ba..fca7b77fc2 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -1,12 +1,11 @@
 # Coq XML Protocol
 
 This document is based on documentation originally written by CJ Bell
-for his [vscoq](https://github.com/siegebell/vscoq/) project.
+for his [vscoq](https://github.com/coq-community/vscoq/) project.
 
 Here, the aim is to provide a "hands on" description of the XML
 protocol that coqtop and IDEs use to communicate. The protocol first appeared 
-with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming 
-versions of Proof General.
+with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/coq-community/vscoq/), and other user interfaces.
 
 A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md).
diff --git a/dev/dune b/dev/dune
index 11e42f97f3..b312a55706 100644
--- a/dev/dune
+++ b/dev/dune
@@ -13,6 +13,8 @@
         ../checker/coqchk.bc
         ../topbin/coqc_bin.bc
         ../ide/coqide_main.bc
-        ; This is not enough as the call to `ocamlfind` will fail :/
+        %{lib:coq.plugins.ltac:ltac_plugin.cma}
+        ; This is not enough, the call to `ocamlfind` may fail if the
+        ; META file is not yet in place :/
         top_printers.cma)
   (action (copy dune-dbg.in dune-dbg)))
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
index 1382f4d1b6..498f167eb1 100755
--- a/dev/dune-dbg.in
+++ b/dev/dune-dbg.in
@@ -7,11 +7,21 @@ case $1 in
         exe=_build/default/checker/coqchk.bc
         ;;
     coqide)
+        shift
         exe=_build/default/ide/coqide_main.bc
         ;;
-    *)
+    coqc)
+        shift
         exe=_build/default/topbin/coqc_bin.bc
         ;;
+    coqtop)
+        shift
+        exe=_build/default/topbin/coqtop_byte_bin.bc
+        ;;
+    *)
+        echo "First argument must be one of {coqc,coqtop,checker,coqide}"
+        exit 1
+        ;;
 esac
 
 emacs="${INSIDE_EMACS:+-emacs}"
diff --git a/dev/dune_db_408 b/dev/dune_db_408
new file mode 100644
index 0000000000..3bf13da62d
--- /dev/null
+++ b/dev/dune_db_408
@@ -0,0 +1,25 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer config.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer gramlib.cma
+load_printer byterun.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer vernac.cma
+load_printer stm.cma
+load_printer toplevel.cma
+
+load_printer ltac_plugin.cma
+load_printer top_printers.cma
+
+source top_printers.dbg
diff --git a/dev/dune_db_409 b/dev/dune_db_409
new file mode 100644
index 0000000000..1267fd5393
--- /dev/null
+++ b/dev/dune_db_409
@@ -0,0 +1,24 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer config.cma
+load_printer clib.cma
+load_printer lib.cma
+load_printer gramlib.cma
+load_printer byterun.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer vernac.cma
+load_printer stm.cma
+load_printer toplevel.cma
+
+load_printer ltac_plugin.cma
+load_printer top_printers.cma
+
+source top_printers.dbg
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 224601bbce..553696410c 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -33,6 +33,6 @@ echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
 echo Checking ocamlformat
-dune build @fmt || CODE=1
+make -f Makefile.dune fmt || CODE=1
 
 exit $CODE
diff --git a/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh
new file mode 100755
index 0000000000..dbf54d7f0a
--- /dev/null
+++ b/dev/tools/pin-ci.sh
@@ -0,0 +1,46 @@
+#!/usr/bin/env bash
+
+# Use this script to pin the commit used by the developments tracked by the CI
+
+OVERLAYS="./dev/ci/ci-basic-overlay.sh"
+
+process_development() {
+  local DEV=$1
+  local REPO_VAR="${DEV}_CI_GITURL"
+  local REPO=${!REPO_VAR}
+  local BRANCH_VAR="${DEV}_CI_REF"
+  local BRANCH=${!BRANCH_VAR}
+  if [[ -z "$BRANCH" ]]
+  then
+    echo "$DEV has no branch set, skipping"
+    return 0
+  fi
+  if [[ $BRANCH =~ ^[a-f0-9]{40}$ ]]
+  then
+    echo "$DEV is already set to hash $BRANCH, skipping"
+    return 0
+  fi
+  echo "Resolving $DEV as $BRANCH from $REPO"
+  local HASH=$(git ls-remote --heads $REPO $BRANCH | cut -f 1)
+  if [[ -z "$HASH" ]]
+  then
+    echo "Could not resolve reference $BRANCH for $DEV (something went wrong), skipping"
+    return 0
+  fi
+  read -p "Expand $DEV from $BRANCH to $HASH? [y/N] " -n 1 -r
+  echo
+  if [[ $REPLY =~ ^[Yy]$ ]]; then
+    # use -i.bak to be compatible with MacOS; see, e.g., https://stackoverflow.com/a/7573438/377022
+    sed -i.bak -e "s/$BRANCH_VAR:=$BRANCH/$BRANCH_VAR:=$HASH/" $OVERLAYS
+  fi
+}
+
+# Execute the script to set the overlay variables
+. $OVERLAYS
+
+# Find all variables declared in the base overlay of the form *_CI_GITURL
+for REPO_VAR in $(compgen -A variable | grep _CI_GITURL)
+do
+  DEV=${REPO_VAR%_CI_GITURL}
+  process_development $DEV
+done
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 835c20a4f7..f640a33773 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -254,7 +254,9 @@ let ppenvwithcst e = pp
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
-let ppobj obj = Format.print_string (Libobject.object_tag obj)
+let ppobj obj =
+  let Libobject.Dyn.Dyn (tag, _) = obj in
+  Format.print_string (Libobject.Dyn.repr tag)
 
 let cnt = ref 0