7 files changed, 53 insertions, 18 deletions
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 919e2a735f..16c4ac37d9 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -4,10 +4,33 @@ This directory provides Docker images to be used by Coq's CI. The
 images do support Docker autobuild on `hub.docker.com` and Gitlab's
 private registry.
 
-Gitlab CI will build and tag a Docker by default for every job if the
-`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this
-variable is usually set to `false` indeed to avoid booting a useless
-job.
+The Gitlab CI will build a docker image unless the CI environment variable
+`SKIP_DOCKER` is set to `true`. This image will be
+stored in the [Gitlab container registry](https://gitlab.com/coq/coq/container_registry)
+under the name given by the `CACHEKEY` variable from
+the [Gitlab CI configuration file](../../../.gitlab-ci.yml).
+
+In Coq's default CI, `SKIP_DOCKER` is set so as to avoid running a lengthy redundant job.
+
+It can be used to regenerate a fresh Docker image on Gitlab through the following steps.
+- Change the `CACHEKEY` variable to a fresh name in the CI configuration in a new commit.
+- Push this commit to a Github PR. This will trigger a Gitlab CI run that will
+  immediately fail, as the Docker image is missing and the `SKIP_DOCKER`
+  default value prevents rebuilding the image.
+- Run a new pipeline on Gitlab with that PR branch, using the green "Run pipeline"
+  button on the [web interface](https://gitlab.com/coq/coq/pipelines),
+  with the `SKIP_DOCKER` environment variable set to `false`. This will run a `docker-boot` process, and
+  once completed, a new Docker image will be available in the container registry,
+  with the name set in `CACHEKEY`.
+- Any pipeline with the same `CACHEKEY` will now automatically reuse that
+  image without rebuilding it from scratch.
+
+For documentation purposes, we also require keeping in sync the `CACHEKEY` comment
+from the first line of the [Dockerfile](bionic_coq/Dockerfile) in the same
+commit.
+
+In case you do not have the rights to run Gitlab CI pipelines, you should ask
+the ci-maintainers Github team to do it for you.
 
 ## Manual Building
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index edca83c6ef..1cad46cd89 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-09-20-V01"
+# CACHEKEY: "bionic_coq-V2019-11-05-V01"
 # ^^ 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 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.7.0"
+    BASE_ONLY_OPAM="elpi.1.8.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6"
diff --git a/dev/ci/user-overlays/09867-primitive-floats.sh b/dev/ci/user-overlays/09867-primitive-floats.sh
new file mode 100644
index 0000000000..a0e9085afd
--- /dev/null
+++ b/dev/ci/user-overlays/09867-primitive-floats.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9867" ] || [ "$CI_BRANCH" = "primitive-floats" ]; then
+
+    unicoq_CI_REF=primitive-floats
+    unicoq_CI_GITURL=https://github.com/validsdp/unicoq
+
+    elpi_CI_REF=primitive-floats
+    elpi_CI_GITURL=https://github.com/validsdp/coq-elpi
+
+    coqhammer_CI_REF=primitive-floats
+    coqhammer_CI_GITURL=https://github.com/validsdp/coqhammer
+
+fi
diff --git a/dev/ci/user-overlays/10358-gares-elpi13.sh b/dev/ci/user-overlays/10358-gares-elpi13.sh
deleted file mode 100644
index d2ba9b5ddf..0000000000
--- a/dev/ci/user-overlays/10358-gares-elpi13.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10358" ] || [ "$CI_BRANCH" = "elpi-13-coq" ]; then
-
-    elpi_CI_REF="elpi-13-coq"
-    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh
new file mode 100644
index 0000000000..f4840c2a83
--- /dev/null
+++ b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then
+
+    equations_CI_REF=proof+private_entry
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/10738-gares-elpi1.7.sh b/dev/ci/user-overlays/10738-gares-elpi1.7.sh
deleted file mode 100644
index 8922badf90..0000000000
--- a/dev/ci/user-overlays/10738-gares-elpi1.7.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "10738" ] || [ "$CI_BRANCH" = "elpi1.7" ]; then
-
-    elpi_CI_REF="coq-master+elpi1.7"
-    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/11051-gares-elpi-1.8.sh b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh
new file mode 100644
index 0000000000..7845654375
--- /dev/null
+++ b/dev/ci/user-overlays/11051-gares-elpi-1.8.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11051" ] || [ "$CI_BRANCH" = "elpi-1.8" ]; then
+
+    elpi_CI_REF="coq-master+v1.2"
+    elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
+
+fi