[circle] Use Docker image from Gitlab registry.

6 files changed, 21 insertions, 48 deletions

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 79f83d472..4d2fb1a4d 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -8,10 +8,11 @@ defaults:
     # reference syntax)
     working_directory: ~/coq
     docker:
-      - image: coqci/base:V2018-05-07-V2
+      - image: $CI_REGISTRY_IMAGE:$CACHEKEY
 
   environment: &envvars
-    NATIVE_COMP: "yes"
+    CACHEKEY: "bionic_coq-V2018-05-07-V2"
+    CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq
 
 version: 2
 
@@ -46,7 +47,9 @@ before_script: &before_script
         paths:
           - coq/
 
-  environment: *envvars
+  environment:
+    <<: *envvars
+    NATIVE_COMP: "yes"
 
 .ci-template: &ci-template
   <<: *params
@@ -63,6 +66,7 @@ before_script: &before_script
         root: *workspace
         paths:
           - coq/
+  environment: *envvars
 
 # Defines individual jobs, see the workflows section below for job orchestration
 jobs:
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index c010da4cf..07777441f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,7 +9,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: bionic_coq-V2018-05-07-V2
+  CACHEKEY: "bionic_coq-V2018-05-07-V2"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/dev/ci/README.md b/dev/ci/README.md
index dee3d2aff..ed3442e0d 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -141,7 +141,6 @@ no OCaml warnings build Coq in parallel with other tests.
 
 ### GitLab and Windows
 
-
 If your repository has access to runners tagged `windows`, setting the
 secret variable `WINDOWS` to `enabled` will add jobs building Windows
 versions of Coq (32bit and 64bit).
@@ -155,6 +154,10 @@ System and opam packages are installed in a Docker image. The image is
 automatically built and uploaded to your GitLab registry, and is
 loaded by subsequent jobs.
 
+**IMPORTANT**: When updating Coq's CI docker image, you must modify
+the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`,
+and `Dockerfile`.
+
 The Docker building job reuses the uploaded image if it is available,
 but if you wish to save more time you can skip the job by setting
 `SKIP_DOCKER` to `true`.
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 8e677f6f2..919e2a735 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -1,37 +1,13 @@
 ## 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`
+images do support Docker autobuild on `hub.docker.com` and Gitlab's
+private registry.
 
-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.
+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.
 
 ## Manual Building
 
@@ -47,10 +23,6 @@ To upload/push to your hub:
   + `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>`
@@ -62,4 +34,3 @@ 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
index 689d203a1..a1178ee2a 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,3 +1,6 @@
+# CACHEKEY: "bionic_coq-V2018-05-07-V2"
+# ^^ Update when modifying this file.
+
 FROM ubuntu:bionic
 LABEL maintainer="e@x80.org"
 
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
deleted file mode 100755
index 307680aa5..000000000
--- a/dev/ci/docker/bionic_coq/hooks/post_push
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-COQCI_VERSION=V2018-05-07-V2
-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