6 files changed, 37 insertions, 273 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index b1c752ba60..859b3e3166 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -921,69 +921,6 @@ function make_gtk_sourceview3 {
   build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/3.24  gtksourceview-3.24.11  tar.xz  make_arch_pkg_config
 }
 
-##### FLEXDLL FLEXLINK #####
-
-# Note: there is a circular dependency between flexlink and ocaml (resolved in Ocaml 4.03.)
-# For MinGW it is not even possible to first build an Ocaml without flexlink support,
-# Because Makefile.nt doesn't support this. So we have to use a binary flexlink.
-# One could of cause do a bootstrap run ...
-
-# Install flexdll objects
-
-function install_flexdll {
-  cp flexdll.h "$PREFIXMINGW/include"
-  if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
-    cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin"
-    cp flexdll*_mingw.o "$PREFIXOCAML/bin"
-  elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
-    cp flexdll*_mingw64.o "/usr/$TARGET_ARCH/bin"
-    cp flexdll*_mingw64.o "$PREFIXOCAML/bin"
-  else
-    echo "Unknown target architecture"
-    return 1
-  fi
-}
-
-# Install flexlink
-
-function install_flexlink {
-  cp flexlink.exe "/usr/$TARGET_ARCH/bin"
-
-  cp flexlink.exe "$PREFIXOCAML/bin"
-}
-
-# Get binary flexdll flexlink for building OCaml
-# An alternative is to first build an OCaml without shared library support and build flexlink with it
-
-function get_flex_dll_link_bin {
-  if build_prep https://github.com/alainfrisch/flexdll/releases/download/0.37/ flexdll-bin-0.37 zip 1 ; then
-    install_flexdll
-    install_flexlink
-    build_post
-  fi
-}
-
-# Build flexdll and flexlink from sources after building OCaml
-
-function make_flex_dll_link {
-  if build_prep https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 ; then
-    if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
-      # shellcheck disable=SC2086
-      log1 make $MAKE_OPT build_mingw flexlink.exe
-    elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
-      # shellcheck disable=SC2086
-      log1 make $MAKE_OPT build_mingw64 flexlink.exe
-    else
-      echo "Unknown target architecture"
-      return 1
-    fi
-    install_flexdll
-    install_flexlink
-    log2 make clean
-    build_post
-  fi
-}
-
 ##### LN replacement #####
 
 # Note: this does support symlinks, but symlinks require special user rights on Windows.
@@ -1016,39 +953,22 @@ function make_arch_pkg_config {
 ##### OCAML #####
 
 function make_ocaml {
-  get_flex_dll_link_bin
-  if build_prep https://github.com/ocaml/ocaml/archive 4.07.1 tar.gz 1 ocaml-4.07.1 ; then
-    # See README.win32.adoc
-    cp config/m-nt.h byterun/caml/m.h
-    cp config/s-nt.h byterun/caml/s.h
-    if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
-        cp config/Makefile.mingw config/Makefile
-    elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
-        cp config/Makefile.mingw64 config/Makefile
-    else
-        echo "Unknown target architecture"
-        return 1
-    fi
+  if build_prep https://github.com/ocaml/ocaml/archive 4.08.1 tar.gz 1 ocaml-4.08.1 ; then
+    # see https://github.com/ocaml/ocaml/blob/4.08/README.win32.adoc
 
-    # Prefix is fixed in make file - replace it with the real one
-    # TODO: this might not work if PREFIX contains spaces
-    sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile
+    # get flexdll sources into folder ./flexdll
+    get_expand_source_tar https://github.com/alainfrisch/flexdll/archive 0.37 tar.gz 1 flexdll-0.37 flexdll
 
     # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder
-    # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path:
-    # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
-    # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
-    # So we put an explicit path in there
-    sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile
-
-    # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT
-    # I verified that 4.02.3 still doesn't support parallel build
-    log2 make world -f Makefile.nt
-    log2 make bootstrap -f Makefile.nt
-    log2 make opt -f Makefile.nt
-    log2 make opt.opt -f Makefile.nt
-    log2 make install -f Makefile.nt
-    # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development
+    logn configure ./configure --build=i686-pc-cygwin --host="$TARGET_ARCH" --prefix="$PREFIXOCAML" --libdir="$PREFIXOCAML/libocaml"
+
+    log2 make flexdll $MAKE_OPT
+    # Note the next command might change after 4.09.x to just make
+    # see        https://github.com/ocaml/ocaml/blob/4.09/README.win32.adoc
+    # compare to https://github.com/ocaml/ocaml/blob/4.10/README.win32.adoc
+    log2 make world.opt $MAKE_OPT
+    log2 make flexlink.opt $MAKE_OPT
+    log2 make install $MAKE_OPT
 
     # Move license files and other into into special folder
     if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
@@ -1065,7 +985,6 @@ function make_ocaml {
 
     build_post
   fi
-  make_flex_dll_link
 }
 
 ##### OCAML EXTRA TOOLS #####
@@ -1099,7 +1018,7 @@ function make_num {
 
 function make_ocamlbuild {
   make_ocaml
-  if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then
+  if build_prep https://github.com/ocaml/ocamlbuild/archive 0.14.0 tar.gz 1 ocamlbuild-0.14.0; then
     log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib
     log1 make $MAKE_OPT
     log2 make install
@@ -1112,6 +1031,7 @@ function make_ocamlbuild {
 function make_findlib {
   make_ocaml
   make_ocamlbuild
+  # Note: latest is 1.8.1 but http://projects.camlcity.org/projects/dl/findlib-1.8.1/doc/README says this is for OCaml 4.09
   if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then
     logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf"
     # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 87122e0fb5..f04de0ce6c 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -209,7 +209,7 @@
 ########################################################################
 # bedrock2
 ########################################################################
-: "${bedrock2_CI_REF:=master}"
+: "${bedrock2_CI_REF:=tested}"
 : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}"
 : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}"
 
diff --git a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
new file mode 100644
index 0000000000..f41271804a
--- /dev/null
+++ b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11338" ] || [ "$CI_BRANCH" = "rm-global-uses-evd" ]; then
+
+    unicoq_CI_REF=rm-global-uses-evd
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+    equations_CI_REF=rm-global-uses-evd
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
deleted file mode 100644
index 66f5a96802..0000000000
--- a/dev/doc/MERGING.md
+++ /dev/null
@@ -1,177 +0,0 @@
-# Merging changes in Coq
-
-This document describes how patches, submitted as pull requests (PRs) on the
-`master` branch, should be merged into the main repository
-(https://github.com/coq/coq).
-
-## Code owners
-
-The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of
-the code. Sometime there is one principal maintainer and one or several
-secondary maintainer(s). Sometimes, it is a team of code owners and all of its
-members act as principal maintainers for the component.
-
-When a PR is submitted, GitHub will automatically ask the principal
-maintainer (or the code owner team) for a review. If the PR touches several
-parts, all the corresponding owners will be asked for a review.
-
-Maintainers are never assigned as reviewer on their own PRs.
-
-If a principal maintainer submits a PR or is a co-author of a PR that is
-submitted and this PR changes the component they own, they must request a
-review from a secondary maintainer. They can also delegate the review if they
-know they are not available to do it.
-
-## Reviewing
-
-When maintainers receive a review request, they are expected to:
-
-* Put their name in the assignee field, if they are in charge of the component
-  that is the main target of the patch (or if they are the only maintainer asked
-  to review the PR).
-* Review the PR, approve it or request changes.
-* If they are the assignee, check if all reviewers approved the PR. If not,
-  regularly ping the author (if changes should be implemented) or the reviewers
-  (if reviews are missing). The assignee ensures that any requests for more
-  discussion have been granted. When the discussion has converged and ALL
-  REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging
-  process described below.
-
-To know what files you are a code owner of in a large PR, you can run
-`dev/tools/check-owners-pr.sh xxxx`. Results are unfortunately imperfect.
-
-When a PR received lots of comments or if the PR has not been opened for long
-and the assignee thinks that some other developers might want to comment,
-it is recommended that they announce their intention to merge and wait a full
-working day (or more if deemed useful) before the actual merge, as a sort of
-last call for comments.
-
-In all cases, maintainers can delegate reviews to the other maintainers,
-except if it would lead to a maintainer reviewing their own patch.
-
-A maintainer is expected to be reasonably reactive, but no specific timeframe is
-given for reviewing.
-
-When none of the maintainers have commented nor self-assigned a PR in a delay
-of five working days, any maintainer of another component who feels comfortable
-reviewing the PR can assign it to themselves. To prevent misunderstandings,
-maintainers should not hesitate to announce in advance when they shall be
-unavailable for more than five working days.
-
-(*) In case a component is touched in a trivial way (adding/removing one file in
-a `Makefile`, etc), or by applying a systematic refactoring process (global
-renaming for instance) that has been reviewed globally, the assignee can
-say in a comment they think a review is not required from every code owner and
-proceed with the merge.
-
-### Breaking changes
-
-If the PR breaks compatibility of some external projects in CI, then fixes to
-those external projects should have been prepared (cf. the relevant sub-section
-in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
-with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
-
-Moreover the PR author *must* add an entry to the [unreleased
-changelog](../../doc/changelog/README.md) or to the
-[`dev/doc/changes.md`](changes.md) file.
-
-If overlays are missing, ask the author to prepare them and label the PR with
-the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
-
-When fixes are ready, there are two cases to consider:
-
-- For patches that are backward compatible (best scenario), you should get the
-  external project maintainers to integrate them before merging the PR.
-- For patches that are not backward compatible (which is often the case when
-  patching plugins after an update to the Coq API), you can proceed to merge
-  the PR and then notify the external project maintainers they can merge the
-  patch.
-
-## Merging
-
-Once all reviewers approved the PR, the assignee is expected to check that CI
-completed without relevant failures, and that the PR comes with appropriate
-documentation and test cases. If not, they should leave a comment on the PR and
-put the appropriate label. Otherwise, they are expected to merge the PR using the
-[merge script](../tools/merge-pr.sh).
-
-When CI has a few failures which look spurious, restarting the corresponding
-jobs is a good way of ensuring this was indeed the case.
-To restart a job on AppVeyor, you should connect using your GitHub
-account; being part of the Coq organization on GitHub should give you the
-permission to do so.
-To restart a job on GitLab CI, you should sign into GitLab (this can be done
-using a GitHub account); if you are part of the
-[Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry"
-button; otherwise, send a request to join the organization.
-
-When the PR has conflicts, the assignee can either:
-- ask the author to rebase the branch, fixing the conflicts
-- warn the author that they are going to rebase the branch, and push to the
-  branch directly
-
-In both cases, CI should be run again.
-
-In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR
-is not a candidate for backporting), it is ok to fix
-the conflicts in the merge commit (following the same steps as below), and push
-to `master` directly. DON'T USE the GitHub interface to fix these conflicts.
-
-To merge the PR proceed in the following way
-```
-$ git checkout master
-$ git pull
-$ dev/tools/merge-pr.sh XXXX
-$ git push upstream
-```
-where `XXXX` is the number of the PR to be merged and `upstream` is the name
-of your remote pointing to `git@github.com:coq/coq.git`.
-Note that you are only supposed to merge PRs into `master`. PRs should rarely
-target the stable branch, but when it is the case they are the responsibility
-of the release manager.
-
-This script conducts various checks before proceeding to merge. Don't bypass them
-without a good reason to, and in that case, write a comment in the PR thread to
-explain the reason.
-
-Maintainers MUST NOT merge their own patches.
-
-DON'T USE the GitHub interface for merging, since it will prevent the automated
-backport script from operating properly, generates bad commit messages, and a
-messy history when there are conflicts.
-
-### Merge script dependencies
-
-The merge script passes option `-S` to `git merge` to ensure merge commits
-are signed. Consequently, it depends on the GnuPG command utility being
-installed and a GPG key being available. Here is a short documentation on
-how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/.
-
-The script depends on a few other utilities. If you are a Nix user, the
-simplest way of getting them is to run `nix-shell` first.
-
-**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG
-is not out of the box. Installing explicitly "pinentry-mac" seems important for
-typing of passphrase to work correctly (see also this
-[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)).
-
-## Addendum for organization admins
-
-### Adding a new code owner individual
-
-If someone is added to the [`CODEOWNERS`](../../.github/CODEOWNERS) file and
-they did not have merging rights before, they should also be added to the
-**@coq/pushers** team. You may do so using
-[this link](https://github.com/orgs/coq/teams/pushers/members?add=true).
-
-Before adding someone to the **@coq/pushers** team, you should ensure that they
-have read the present merging documentation, and explicitly tell them not to
-use the merging button on the GitHub web interface.
-
-### Adding a new code owner team
-
-Go to [that page](https://github.com/orgs/coq/teams/pushers/teams) and click on
-the green "Add a team" button. Use a "-maintainer" suffix for the name of your
-team. You may then add new members to this team (you don't need to add them to
-the **@coq/pushers** team first as this will be done automatically because the
-team you created is a sub-team of **@coq/pushers**).
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 67becb251a..2d187f7bae 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -255,6 +255,18 @@ Conversion machines
   GH issue number: #9925
   risk:
 
+  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
+  summary: broken long multiplication primitive integer emulation layer on 32 bits
+  introduced: e43b176
+  impacted released versions: 8.10.0, 8.10.1, 8.10.2
+  impacted development branches: 8.11
+  impacted coqchk versions: none (no virtual machine in coqchk)
+  fixed in: 4e176a7
+  found by: Soegtrop, Melquiond
+  exploit: test-suite/bugs/closed/bug_11321.v
+  GH issue number: #11321
+  risk: critical, as any BigN computation on 32-bit architectures is wrong
+
   component: "native" conversion machine (translation to OCaml which compiles to native code)
   summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
   introduced: V8.5
diff --git a/dev/doc/shield-icon.png b/dev/doc/shield-icon.png
new file mode 100644
index 0000000000..629e51a819
--- /dev/null
+++ b/dev/doc/shield-icon.png