20 files changed, 78 insertions, 47 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 88d08a1724..d5c6096100 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -73,16 +73,31 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil
 
 If you break external projects that are hosted on GitHub, you can use
 the `create_overlays.sh` script to automatically perform most of the
-above steps. In order to do so, call the script as:
-```
-./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac
-```
-replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR
-number. The script will:
+above steps. In order to do so:
 
-- checkout the contributions and prepare the branch/remote so you can
-  just commit the fixes and push,
-- add the corresponding overlay file in `dev/ci/user-overlays`.
+- determine the list of failing projects:
+IDs can be found as ci-XXX1 ci-XXX2 ci-XXX3 in the list of GitLab CI failures;
+- for each project XXXi, look in [ci-basic-overlay.sh](https://github.com/coq/coq/blob/master/dev/ci/ci-basic-overlay.sh)
+to see if the corresponding `XXXi_CI_GITURL` is hosted on GitHub;
+- log on GitHub and fork all the XXXi projects hosted there;
+- call the script as:
+
+    ```
+    ./dev/tools/create_overlays.sh ejgallego 9873 XXX1 XXX2 XXX3
+    ```
+
+    replacing `ejgallego` by your GitHub nickname, `9873` by the actual PR
+number, and selecting the XXXi hosted on GitHub. The script will:
+
+    + checkout the contributions and prepare the branch/remote so you can
+      just commit the fixes and push,
+    + add the corresponding overlay file in `dev/ci/user-overlays`;
+
+- go to `_build_ci/XXXi` to prepare your overlay
+(you can test your modifications by using `make -C ../.. ci-XXXi`)
+and push using `git push ejgallego` (replacing `ejgallego` by your GitHub nickname);
+- finally push the `dev/ci/user-overlays/9873-elgallego-YYY.sh` file on your Coq fork
+(replacing `9873` by the actual PR number, and `ejgallego` by your GitHub nickname).
 
 For problems related to ML-plugins, if you use `dune build` to build
 Coq, it will actually be aware of the broken contributions and perform
@@ -124,7 +139,7 @@ Currently available artifacts are:
 - the Coq documentation, built in the `doc:*` jobs. When submitting a
   documentation PR, this can help reviewers checking the rendered
   result.  **@coqbot** will automatically post links to these
-  artifacts in the PR checks section.  Furthemore, these artifacts are
+  artifacts in the PR checks section.  Furthermore, these artifacts are
   automatically deployed at:
 
   + Coq's Reference Manual [master branch]:
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index f7a8851af7..b87a9c0392 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -46,9 +46,9 @@
 : "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}"
 : "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}"
 
-: "${Corn_CI_REF:=master}"
-: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}"
-: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}"
+: "${corn_CI_REF:=master}"
+: "${corn_CI_GITURL:=https://github.com/coq-community/corn}"
+: "${corn_CI_ARCHIVEURL:=${corn_CI_GITURL}/archive}"
 
 ########################################################################
 # Iris
@@ -59,19 +59,19 @@
 : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}"
 : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
 
-: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
-: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
+: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
+: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}"
 
-: "${lambdaRust_CI_REF:=master}"
-: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
-: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}"
+: "${lambda_rust_CI_REF:=master}"
+: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
+: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}"
 
 ########################################################################
 # HoTT
 ########################################################################
-: "${HoTT_CI_REF:=master}"
-: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}"
-: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}"
+: "${hott_CI_REF:=master}"
+: "${hott_CI_GITURL:=https://github.com/HoTT/HoTT}"
+: "${hott_CI_ARCHIVEURL:=${hott_CI_GITURL}/archive}"
 
 ########################################################################
 # CoqHammer
@@ -83,16 +83,16 @@
 ########################################################################
 # GeoCoq
 ########################################################################
-: "${GeoCoq_CI_REF:=master}"
-: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}"
-: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}"
+: "${geocoq_CI_REF:=master}"
+: "${geocoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}"
+: "${geocoq_CI_ARCHIVEURL:=${geocoq_CI_GITURL}/archive}"
 
 ########################################################################
 # Flocq
 ########################################################################
-: "${Flocq_CI_REF:=master}"
-: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}"
-: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
+: "${flocq_CI_REF:=master}"
+: "${flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}"
+: "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
 # coq-tools
diff --git a/dev/ci/ci-coq-tools.sh b/dev/ci/ci-coq_tools.sh
index 9c95c49c9f..9c95c49c9f 100755
--- a/dev/ci/ci-coq-tools.sh
+++ b/dev/ci/ci-coq_tools.sh
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
index a0c714884c..ac3978dc8d 100755
--- a/dev/ci/ci-corn.sh
+++ b/dev/ci/ci-corn.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download Corn
+git_download corn
 
-( cd "${CI_BUILD_DIR}/Corn" && ./configure.sh && make && make install )
+( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross_crypto.sh
index 900d12c1dd..900d12c1dd 100755
--- a/dev/ci/ci-cross-crypto.sh
+++ b/dev/ci/ci-cross_crypto.sh
diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext_lib.sh
index 5eb167d97d..5eb167d97d 100755
--- a/dev/ci/ci-ext-lib.sh
+++ b/dev/ci/ci-ext_lib.sh
diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl_pcm.sh
index cb951630c8..cb951630c8 100755
--- a/dev/ci/ci-fcsl-pcm.sh
+++ b/dev/ci/ci-fcsl_pcm.sh
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 811fefda35..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 7a9531216e..a3a704091b 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download Flocq
+git_download flocq
 
-( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
+( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 8c57318477..e4fc983e68 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -5,6 +5,6 @@ ci_dir="$(dirname "$0")"
 
 install_ssralg
 
-git_download GeoCoq
+git_download geocoq
 
-( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make )
+( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index c8e6fe690f..4b92c8cb4d 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download HoTT
+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 && make && make validate )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-lambda_rust.sh
index d99e140bce..1ef0c2cb8f 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-lambda_rust.sh
@@ -5,17 +5,17 @@ ci_dir="$(dirname "$0")"
 
 install_ssreflect
 
-# Setup lambdaRust first
-git_download lambdaRust
+# Setup lambda_rust first
+git_download lambda_rust
 
 # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
-Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
 
 # Setup Iris
-git_download Iris
+git_download iris
 
 # Extract required version of std++
-stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
 
 # Setup std++
 git_download stdpp
@@ -24,7 +24,7 @@ git_download stdpp
 ( cd "${CI_BUILD_DIR}/stdpp" && make && make install )
 
 # Build and validate Iris
-( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install )
+( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install )
 
-# Build lambdaRust
-( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install )
+# Build lambda_rust
+( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math_classes.sh
index ae31a8e7f8..ae31a8e7f8 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math_classes.sh
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-mathcomp.sh
index cae127ee7b..cae127ee7b 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-mathcomp.sh
diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple_io.sh
index e7bcd80de7..e7bcd80de7 100755
--- a/dev/ci/ci-simple-io.sh
+++ b/dev/ci/ci-simple_io.sh
diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi_raft.sh
index 3bcd52c464..3bcd52c464 100755
--- a/dev/ci/ci-verdi-raft.sh
+++ b/dev/ci/ci-verdi_raft.sh
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e240ea3ba1..9ee6496ee5 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-13-V69"
+# CACHEKEY: "bionic_coq-V2020-05-06-V70"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -39,7 +39,7 @@ ENV COMPILER="4.05.0"
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.10.2"
+    BASE_ONLY_OPAM="elpi.1.11.0"
 
 # 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/12227-ppedrot-refiner-rm-v82.sh b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
new file mode 100644
index 0000000000..0f8daf418c
--- /dev/null
+++ b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then
+
+    equations_CI_REF="refiner-rm-v82"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/12267-gares-elpi-1.11.sh b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh
new file mode 100644
index 0000000000..ceb7afe3d1
--- /dev/null
+++ b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12267" ] || [ "$CI_BRANCH" = "elpi-1.11" ]; then
+
+    elpi_CI_REF="coq-master+elpi-1.11"
+    elpi_hb_CI_REF="coq-master+elpi.11"
+
+fi
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 58c2fcc68a..ceb390c02c 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -131,8 +131,12 @@ in time.
   the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq)
   (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built).
 - [ ] Draft a release on GitHub.
-- [ ] Get `@maximedenes` to sign the Windows and MacOS packages and
-  upload them on GitHub.
+- [ ] Sign the Windows and MacOS packages and upload them on GitHub.
+  + The Windows packages must be signed by the Inria IT security service. They
+    should be sent as a link to the binary together with its SHA256 hash in a
+    signed e-mail, via our local contact (currently `@maximedenes`).
+  + The MacOS packages should be signed by our own certificate, by sending them
+    to `@maximedenes`. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases).
 - [ ] Prepare a page of news on the website with the link to the GitHub release
   (see [coq/www#63](https://github.com/coq/www/pull/63)).
 - [ ] Upload the new version of the reference manual to the website.