2 files changed, 33 insertions, 10 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..b8f9d99702 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-12-08-V82"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -8,7 +8,7 @@ ENV DEBIAN_FRONTEND="noninteractive"
 
 RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of the image, the test-suite and external projects
-        m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \
+        m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \
         # Dependencies of lablgtk (for CoqIDE)
         libgtksourceview-3.0-dev \
         # Dependencies of stdlib and sphinx doc
@@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.4/opam-2.0.4-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -37,9 +37,9 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \
+ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.0 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"
@@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 # EDGE switch
 ENV COMPILER_EDGE="4.09.0" \
     COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \
-    BASE_OPAM_EDGE="dune-release.1.3.2"
+    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.