[gitlab] [circleci] Use a Custom Docker Image as base CI setup.

We provide a custom `Dockerfile` for Coq's CI system, based on
`ubuntu:bionic`. The image includes the required set of packages and
OPAM switches.

This greatly simplifies the Gitlab and Circle scripts, at the cost of
having to push a Docker build for them to depend on.

Travis is not included in this PR as it requires significant more
refactoring due to lack of native Docker support.

This is work in progress but ready, a build hook is used so the image
is properly tagged in the Docker autobuilder.

We need to improve the autobuilder setup but this last point requires
some design on how to trigger it.

Fixes #7383

7 files changed, 172 insertions, 260 deletions

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 451b711be..07b728edf 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -8,83 +8,29 @@ defaults:
     # reference syntax)
     working_directory: ~/coq
     docker:
-      - image: ocaml/opam:ubuntu
+      - image: coqci/base:V2018-05-05
 
   environment: &envvars
-    # required by some of the targets, e.g. compcert, passed for
-    # instance to opam to configure the number of parallel jobs
-    # allowed
-    NJOBS: 2
-    COMPILER: "system"
-    CAMLP5_VER: "6.14"
     NATIVE_COMP: "yes"
 
-    # some useful values
-    TIMING_PACKAGES: &timing-packages "time python"
-
 version: 2
 
 before_script: &before_script
-  name: Install system packages
+  name: Setup OPAM Switch
   command: |
     echo export TERM=xterm >> ~/.profile
     source ~/.profile
-    printenv
-    if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi
     echo . ~/.profile >> $BASH_ENV
-
-opam-switch: &opam-switch
-  name: Select opam switch
-  command: |
-    opam switch ${COMPILER}
+    printenv | sort
+    opam switch "$COMPILER"
     opam config list
     opam list
 
-.opam-boot-template: &opam-boot-template
-  <<: *params
-  steps:
-    - checkout
-    - run: *before_script
-    - run:
-        name: Cache selection
-        command: |
-          # We can't use environment variables in cache names
-          # So put it in a file and use the checksum
-          echo "$COMPILER" > COMPILER
-    - restore_cache:
-        keys:
-          - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}-
-    - run:
-        name: Update opam lists
-        command: |
-          opam repository set-url default https://opam.ocaml.org
-          opam update
-    - run:
-        name: Install opam packages
-        command: |
-          opam switch -j ${NJOBS} ${COMPILER}
-          opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
-    - run:
-        name: Clean cache
-        command: |
-          rm -rf ~/.opam/log/
-    - save_cache:
-        key: coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}-
-        paths:
-          - ~/.opam
-    - persist_to_workspace:
-        root: &workspace ~/
-        paths:
-          - .opam/
-
 .build-template: &build-template
   <<: *params
   steps:
     - checkout
     - run: *before_script
-    - attach_workspace: &attach_workspace
-        at: *workspace
-    - run: *opam-switch
     - run: &build-configure
         name: Configure
         command: |
@@ -96,7 +42,7 @@ opam-switch: &opam-switch
           make -j ${NJOBS}
           make test-suite/misc/universes/all_stdlib.v
     - persist_to_workspace:
-        root: *workspace
+        root: &workspace ~/
         paths:
           - coq/
 
@@ -106,7 +52,9 @@ opam-switch: &opam-switch
   <<: *params
   steps:
     - run: *before_script
-    - attach_workspace: *attach_workspace
+    - attach_workspace: &attach_workspace
+        at: *workspace
+
     - run:
         name: Test
         command: |
@@ -115,19 +63,10 @@ opam-switch: &opam-switch
         root: *workspace
         paths:
           - coq/
-  environment: &ci-template-vars
-    <<: *envvars
-    EXTRA_PACKAGES: *timing-packages
 
 # Defines individual jobs, see the workflows section below for job orchestration
 jobs:
 
-  opam-boot:
-    <<: *opam-boot-template
-    environment:
-      <<: *envvars
-      EXTRA_OPAM: "ocamlgraph elpi"
-
   # Build and prepare test environment
   build: *build-template
 
@@ -136,24 +75,15 @@ jobs:
 
   color:
     <<: *ci-template
-    environment:
-      <<: *ci-template-vars
-      EXTRA_PACKAGES: *timing-packages
 
   compcert:
     <<: *ci-template
 
   coq-dpdgraph:
     <<: *ci-template
-    environment:
-      <<: *ci-template-vars
-      EXTRA_PACKAGES: "time python autoconf automake"
 
   coquelicot:
     <<: *ci-template
-    environment:
-      <<: *ci-template-vars
-      EXTRA_PACKAGES: "time python autoconf automake"
 
   elpi:
     <<: *ci-template
@@ -172,15 +102,9 @@ jobs:
 
   fiat-parsers:
     <<: *ci-template
-    environment:
-      <<: *ci-template-vars
-      EXTRA_PACKAGES: *timing-packages
 
   flocq:
     <<: *ci-template
-    environment:
-      <<: *ci-template-vars
-      EXTRA_PACKAGES: "time python autoconf automake"
 
   math-classes:
     <<: *ci-template
@@ -193,9 +117,6 @@ jobs:
 
   hott:
     <<: *ci-template
-    environment:
-      <<: *ci-template-vars
-      EXTRA_PACKAGES: "time python autoconf automake"
 
   iris-lambda-rust:
     <<: *ci-template
@@ -214,9 +135,6 @@ jobs:
 
   sf:
     <<: *ci-template
-    environment:
-      <<: *ci-template-vars
-      EXTRA_PACKAGES: "time python wget"
 
   unimath:
     <<: *ci-template
@@ -226,14 +144,11 @@ jobs:
 
 workflows:
   version: 2
+
   # Run on each push
   main:
     jobs:
-      - opam-boot
-
-      - build:
-          requires:
-            - opam-boot
+      - build
 
       - bignums: &req-main
           requires:
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d16dc5b78..12d3a87b2 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,76 +1,35 @@
-image: ubuntu:bionic
+image: coqci/base:V2018-05-05
 
 stages:
-  - opam-boot
   - build
   - test
 
 # some default values
 variables:
-  # Format: $IMAGE-V$DATE-$HOUR-$MINUTE
-  CACHEKEY: bionic-V2018-04-29-00-50
-  DEBIAN_FRONTEND: "noninteractive"
-  NJOBS: "2"
-  COMPILER: "4.02.3"
-  CAMLP5_VER: "6.14"
-  OPAMROOT: "$CI_PROJECT_DIR/.opamcache"
-  OPAMROOTISOK: "true"
-
-  # some useful values
-  COMPILER_32BIT: "4.02.3+32bit"
-
-  COMPILER_BLEEDING_EDGE: "4.06.1"
-  CAMLP5_VER_BLEEDING_EDGE: "7.05"
-
-  TIMING_PACKAGES: "time python3"
-
-  COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev"
-  #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386"
-  COQIDE_OPAM: "lablgtk.2.18.5 conf-gtksourceview.2"
-  COQIDE_OPAM_BE: "lablgtk.2.18.6 conf-gtksourceview.2"
-  COQDOC_PACKAGES: "texlive-latex-extra texlive-fonts-recommended hevea python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip"
-  SPHINX_PACKAGES: "antlr4-python3-runtime"
-  ELPI_OPAM: "elpi"
+  # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
+  # for reference]
+  CACHEKEY: bionic_coq-V2018-05-03
+  # By default, jobs run in the base switch; override to select another switch
+  OPAM_SWITCH: "base"
+  # Used to select special compiler switches such as flambda, 32bits, etc...
+  OPAM_VARIANT: ""
 
 before_script:
   - cat /proc/{cpu,mem}info || true
   - ls -a # figure out if artifacts are around
-  - printenv
-#  - if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi
-  - apt-get update -qq && apt-get install -y -qq m4 opam ${EXTRA_PACKAGES}
-  # This should be replaced by standard debian packages once python3-antlr4 makes to the archive.
-  - if [ -n "${PIP_PACKAGES}" ]; then pip3 install ${PIP_PACKAGES}; fi
-  # if no cache running opam config fails!
-  - if [ -d .opamcache ]; then eval $(opam config env); fi
-
-################ OPAM SYSTEM ######################
-# - use cache between pipelines
-# - use artifacts between jobs
-#   (in https://gitlab.com/SkySkimmer/coq/-/jobs/63255417
-#    the cache wasn't available at the build step)
-# every non opam-boot job must set dependencies (for ci it's in the template)
-# otherwise all opam-boot artifacts are used together and we get some random switch
-
-# set cache key when using
-.opam-boot-template: &opam-boot-template
-  stage: opam-boot
-  artifacts:
-    name: "opam-$COMPILER"
-    paths:
-      - .opamcache
-    expire_in: 1 week
-  script:
-    - opam init -a -y -j $NJOBS --compiler=${COMPILER} default https://opam.ocaml.org
-    - eval $(opam config env)
-    - opam update
-    - opam config list
-    - opam list
-    - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM}
-    - rm -rf ~/.opam/log/
-    - opam list
-
-# TODO figure out how to build doc for installed coq
-# set dependencies when using
+  - printenv | sort
+  - declare -A switch_table
+  - switch_table=( ["base"]="$COMPILER" ["be"]="$COMPILER_BE" )
+  - opam switch -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
+  - eval $(opam config env)
+  - opam list
+  - opam config list
+
+################ GITLAB CACHING ######################
+# - use artifacts between jobs                       #
+######################################################
+
+# TODO figure out how to build doc for installed Coq
 .build-template: &build-template
   stage: build
   artifacts:
@@ -80,21 +39,16 @@ before_script:
       - config/Makefile
       - test-suite/misc/universes/all_stdlib.v
     expire_in: 1 week
-  dependencies:
-    - not-a-real-job
   script:
     - set -e
-    - printenv
-    - opam config list
-    - opam list
 
     - echo 'start:coq.config'
     - ./configure -prefix "$(pwd)/_install_ci" ${EXTRA_CONF}
     - echo 'end:coq.config'
 
     - echo 'start:coq.build'
-    - make -j ${NJOBS} byte
-    - make -j ${NJOBS}
+    - make -j "$NJOBS" byte
+    - make -j "$NJOBS"
     - make test-suite/misc/universes/all_stdlib.v
     - echo 'end:coq:build'
 
@@ -106,12 +60,9 @@ before_script:
 
     - set +e
 
-# set dependencies when using
 .warnings-template: &warnings-template
   # keep warnings in test stage so we can test things even when warnings occur
   stage: test
-  dependencies:
-    - not-a-real-job
   script:
     - set -e
 
@@ -120,14 +71,17 @@ before_script:
     - echo 'end:coq.config'
 
     - echo 'start:coq.build'
-    - make -j ${NJOBS} coqocaml
+    - make -j "$NJOBS" coqocaml
     - echo 'end:coq:build'
 
     - set +e
   variables: &warnings-variables
     EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only"
-    EXTRA_PACKAGES: "$COQIDE_PACKAGES"
-    EXTRA_OPAM: "$COQIDE_OPAM"
+
+# every non build job must set dependencies otherwise all build
+# artifacts are used together and we may get some random Coq. To that
+# purpose, we add a spurious dependency `not-a-real-job` that must be
+# overridden otherwise the CI will fail.
 
 # set dependencies when using
 .test-suite-template: &test-suite-template
@@ -140,7 +94,7 @@ before_script:
     # careful with the ending /
     - BIN=$(readlink -f ../_install_ci/bin)/
     - LIB=$(readlink -f ../_install_ci/lib/coq)/
-    - make -j ${NJOBS} BIN="$BIN" LIB="$LIB" all
+    - make -j "$NJOBS" BIN="$BIN" LIB="$LIB" all
   artifacts:
     name: "$CI_JOB_NAME.logs"
     when: on_failure
@@ -163,151 +117,90 @@ before_script:
   script:
     - set -e
     - echo 'start:coq.test'
-    - make -f Makefile.ci -j ${NJOBS} ${TEST_TARGET}
+    - make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET}
     - echo 'end:coq.test'
     - set +e
   dependencies:
-    - opam-boot
     - build
   variables: &ci-template-vars
     TEST_TARGET: "$CI_JOB_NAME"
-    EXTRA_PACKAGES: "$TIMING_PACKAGES"
-
-opam-boot:
-  <<: *opam-boot-template
-  cache:
-    paths: &cache-paths
-      - .opamcache
-    key: "main-$CACHEKEY"
-  variables:
-    EXTRA_OPAM: "$COQIDE_OPAM ocamlgraph $ELPI_OPAM"
-    EXTRA_PACKAGES: "$COQIDE_PACKAGES"
-
-opam-boot:32bit:
-  <<: *opam-boot-template
-  cache:
-    paths: *cache-paths
-    key: "32bit-$CACHEKEY"
-  variables:
-    COMPILER: "$COMPILER_32BIT"
-    EXTRA_PACKAGES: "gcc-multilib"
-
-opam-boot:bleeding-edge:
-  <<: *opam-boot-template
-  cache:
-    paths: *cache-paths
-    key: "be-$CACHEKEY"
-  variables:
-    COMPILER: "$COMPILER_BLEEDING_EDGE"
-    CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
-    EXTRA_PACKAGES: "$COQIDE_PACKAGES"
-    EXTRA_OPAM: "$COQIDE_OPAM_BE"
 
 build:
   <<: *build-template
-  dependencies:
-    - opam-boot
   variables:
     EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
-    EXTRA_PACKAGES: "$COQIDE_PACKAGES $COQDOC_PACKAGES"
-    PIP_PACKAGES: "$SPHINX_PACKAGES"
 
 # no coqide for 32bit: libgtk installation problems
 build:32bit:
   <<: *build-template
-  dependencies:
-    - opam-boot:32bit
   variables:
+    OPAM_VARIANT: "+32bit"
     EXTRA_CONF: "-native-compiler yes"
-    EXTRA_PACKAGES: "gcc-multilib"
 
 build:bleeding-edge:
   <<: *build-template
-  dependencies:
-    - opam-boot:bleeding-edge
   variables:
+    OPAM_SWITCH: be
     EXTRA_CONF: "-native-compiler yes -coqide opt"
-    EXTRA_PACKAGES: "$COQIDE_PACKAGES"
 
 warnings:
   <<: *warnings-template
-  dependencies:
-    - opam-boot
 
 # warnings:32bit:
 #   <<: *warnings-template
 #   variables:
 #     <<: *warnings-variables
-#     EXTRA_PACKAGES: "$gcc-multilib COQIDE_PACKAGES_32BIT"
-#   dependencies:
-#     - opam-boot:32bit
 
 warnings:bleeding-edge:
   <<: *warnings-template
-  dependencies:
-    - opam-boot:bleeding-edge
+  variables:
+    OPAM_SWITCH: be
 
 test-suite:
   <<: *test-suite-template
   dependencies:
-    - opam-boot
     - build
-  variables:
-    EXTRA_PACKAGES: "$TIMING_PACKAGES"
 
 test-suite:32bit:
   <<: *test-suite-template
   dependencies:
-    - opam-boot:32bit
     - build:32bit
   variables:
-    EXTRA_PACKAGES: "gcc-multilib $TIMING_PACKAGES"
+    OPAM_VARIANT: "+32bit"
 
 test-suite:bleeding-edge:
   <<: *test-suite-template
   dependencies:
-    - opam-boot:bleeding-edge
     - build:bleeding-edge
   variables:
-    EXTRA_PACKAGES: "$TIMING_PACKAGES"
+    OPAM_SWITCH: be
 
 validate:
   <<: *validate-template
   dependencies:
-    - opam-boot
     - build
 
 validate:32bit:
   <<: *validate-template
   dependencies:
-    - opam-boot:32bit
     - build:32bit
   variables:
-    EXTRA_PACKAGES: "gcc-multilib"
+    OPAM_VARIANT: "+32bit"
 
 ci-bignums:
   <<: *ci-template
 
 ci-color:
   <<: *ci-template
-  variables:
-    <<: *ci-template-vars
-    EXTRA_PACKAGES: "$TIMING_PACKAGES"
 
 ci-compcert:
   <<: *ci-template
 
 ci-coq-dpdgraph:
   <<: *ci-template
-  variables:
-    <<: *ci-template-vars
-    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"
 
 ci-coquelicot:
   <<: *ci-template
-  variables:
-    <<: *ci-template-vars
-    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"
 
 ci-elpi:
   <<: *ci-template
@@ -315,10 +208,6 @@ ci-elpi:
 ci-equations:
   <<: *ci-template
 
-ci-geocoq:
-  <<: *ci-template
-  allow_failure: true
-
 ci-fcsl-pcm:
   <<: *ci-template
 
@@ -329,24 +218,18 @@ ci-fcsl-pcm:
 
 ci-fiat-parsers:
   <<: *ci-template
-  variables:
-    <<: *ci-template-vars
-    EXTRA_PACKAGES: "$TIMING_PACKAGES"
 
 ci-flocq:
   <<: *ci-template
-  variables:
-    <<: *ci-template-vars
-    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"
 
 ci-formal-topology:
   <<: *ci-template
 
+ci-geocoq:
+  <<: *ci-template
+
 ci-hott:
   <<: *ci-template
-  variables:
-    <<: *ci-template-vars
-    EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf"
 
 ci-iris-lambda-rust:
   <<: *ci-template
@@ -368,9 +251,6 @@ ci-pidetop:
 
 ci-sf:
   <<: *ci-template
-  variables:
-    <<: *ci-template-vars
-    EXTRA_PACKAGES: "$TIMING_PACKAGES wget"
 
 ci-unimath:
   <<: *ci-template
diff --git a/.travis.yml b/.travis.yml
index fce19f9d9..eeb0b800e 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -39,11 +39,11 @@ env:
   - NJOBS=2
   # system is == 4.02.3
   - COMPILER="system"
-  - COMPILER_BE="4.06.0"
+  - COMPILER_BE="4.06.1"
   - CAMLP5_VER=".6.14"
   - CAMLP5_VER_BE=".7.03"
   - FINDLIB_VER=".1.4.1"
-  - FINDLIB_VER_BE=".1.7.3"
+  - FINDLIB_VER_BE=".1.8.0"
   - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6"
   - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6"
   - NATIVE_COMP="yes"
@@ -67,7 +67,7 @@ matrix:
       - TEST_TARGET="ci-color"
     - if: NOT (type = pull_request)
       env:
-      - TEST_TARGET="ci-compcert"
+      - TEST_TARGET="ci-compcert" EXTRA_OPAM="menhir"
     - if: NOT (type = pull_request)
       env:
       - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index fbdeff20c..8d490591b 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
 
 CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert"
 
-opam install -j "$NJOBS" -y menhir
 git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}"
 
 ( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
new file mode 100644
index 000000000..8e677f6f2
--- /dev/null
+++ b/dev/ci/docker/README.md
@@ -0,0 +1,65 @@
+## Overall Docker Setup for Coq's CI.
+
+This directory provides Docker images to be used by Coq's CI. The
+images do support Docker autobuild on `hub.docker.com`
+
+Autobuild is the preferred build method [see below]; if you are a
+member of the `coqci` organization, the automated build will push the
+image to the `coqci/name:$VERSION` tag using a Docker hub hook.
+
+## Updating the Image and Syncronization with CI files
+
+Unfortunately, at this point some manual synchronization is needed
+between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the
+checklist is:
+
+- check the name and version of the image setup in `hooks/post_push`
+  have to match.
+- check `COMPILER` variables do match.
+
+Once you are sure the variables are right, then proceed to trigger an
+autobuild or do a manual build, et voilà !
+
+## Docker Autobuilding.
+
+We provide basic support for auto-building, see:
+
+https://docs.docker.com/docker-cloud/builds/advanced/
+
+If you are member of the `coqci` Docker organization, trigger an
+autobuild in your account and the image will be pushed to it as we
+set the proper tag in `hooks/post_push`.
+
+We still need to figure out how properly setup a more automated,
+organization-wide auto-building process.
+
+## Manual Building
+
+You can also manually build and push any image:
+
+- Build the image `docker build -t base:$VERSION .`
+
+To upload/push to your hub:
+
+- Create a https://hub.docker.com account.
+- Login into your space `docker login --username=$USER`
+- Push the image:
+  + `docker tag base:$VERSION $USER/base:$VERSION`
+  + `docker push $USER/base:$VERSION`
+
+Now your docker image is ready to be used. To upload to `coqci`:
+- `docker tag base:$VERSION coqci/base:$VERSION`
+- `docker push coqci/base:$VERSION`
+
+## Debugging / Misc
+
+To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>`
+
+Each `RUN` command creates an "layer", thus a Docker build is
+incremental and it always help to put things updated more often at the
+end.
+
+## Possible Improvements:
+
+- Use ARG for customizing versions, centralize variable setup;
+- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry .
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
new file mode 100644
index 000000000..5698175c5
--- /dev/null
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -0,0 +1,45 @@
+FROM ubuntu:bionic
+LABEL maintainer="e@x80.org"
+
+ENV DEBIAN_FRONTEND="noninteractive"
+
+RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \
+        libgtk2.0-dev libgtksourceview2.0-dev \
+        texlive-latex-extra texlive-fonts-recommended hevea \
+        python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip
+
+RUN pip3 install antlr4-python3-runtime
+
+# Basic OPAM setup
+ENV NJOBS="2" \
+    OPAMROOT=/root/.opamcache \
+    OPAMROOTISOK="true"
+
+ENV COMPILER="4.02.3" \
+    BASE_OPAM="num ocamlfind jbuilder"
+
+RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update
+
+# Setup of the base switch
+ENV CAMLP5_VER="6.14" \
+    COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" \
+    CI_OPAM="menhir elpi ocamlgraph"
+
+RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
+
+# base+32bit switch
+RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
+
+# BE switch
+ENV COMPILER_BE="4.06.1" \
+    CAMLP5_VER_BE="7.05" \
+    COQIDE_OPAM_BE="lablgtk.2.18.6 conf-gtksourceview.2"
+
+RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
+
+# BE+flambda switch
+RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \
+    opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
new file mode 100755
index 000000000..008ef1af3
--- /dev/null
+++ b/dev/ci/docker/bionic_coq/hooks/post_push
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+COQCI_VERSION=V2018-05-05
+docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
+docker push $DOCKER_REPO:$COQCI_VERSION
+
+docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION
+docker push coqci/base:$COQCI_VERSION