Refactor jobs: Split .opam-build & Create .docker-deploy

* The latter template job is trusted and only runs:
  - in branch master,
  - if all build *and* test jobs were successful
    (major change in the deployment's condition)

* The other jobs are not tagged with "environment: name: deployment",
  so they won't be able to read scoped protected variables.

* href: https://gitlab.com/help/ci/variables/README.md#limiting-environment-scopes-of-variables-premium

1 files changed, 40 insertions, 13 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1423e9b..880d22d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -2,14 +2,15 @@
 # - build stage (e.g. docker build -t mathcomp-dev:$IID_$SLUG_coq-8.7 .)
 #   - choice of the OCaml compiler: var OPAM_SWITCH in {base, edge}
 #     (Dockerfile containing: "opam switch set $compiler && eval $(opam env)")
-#   - master (protected branch) => push on GitLab registry and Docker Hub
-#   - other branches (not tags) => push on GitLab registry
+#   - all branches (not tags) => push on GitLab registry
 #   - GitHub PRs => push on GitLab and report back thanks to @coqbot
 # - test stage (image: mathcomp-dev:$IID_$SLUG_coq-8.6)
 #   - script template foreach project (custom CONTRIB_URL, script)
 #   - jobs foreach project and Coq version (custom COQ_VERSION, CONTRIB_VERSION)
+# - deploy stage (only branch "master" and environment "deployment")
+#   - pull each built image from GitLab registry => push to Docker Hub
 #
-# Config for protected branches:
+# Config for protected environment "deployment":
 # - set vars HUB_REGISTRY, HUB_REGISTRY_USER, HUB_REGISTRY_IMAGE, HUB_TOKEN
 #
 # Remark:
@@ -26,6 +27,7 @@
 stages:
   - build
   - test
+  - deploy
 
 ################
 #### build stage
@@ -61,7 +63,6 @@ make-coq-latest:
     - docker:dind
   variables:
     IMAGE: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_${CI_JOB_NAME}"
-    HUB_IMAGE: "${HUB_REGISTRY_IMAGE}:${CI_JOB_NAME}"
     OPAM_SWITCH: "edge"
   before_script:
     - echo "${CI_JOB_TOKEN}" | docker login -u "${CI_REGISTRY_USER}" --password-stdin "${CI_REGISTRY}"
@@ -69,15 +70,6 @@ make-coq-latest:
     - docker build --pull --build-arg=coq_image="coqorg/${CI_JOB_NAME//-/:}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" .
     - docker push "${IMAGE}"
     - docker logout "${CI_REGISTRY}"
-    - |
-      if [ -n "${HUB_REGISTRY_IMAGE}" ]; then
-        set -e
-        echo "${HUB_TOKEN}" | docker login -u "${HUB_REGISTRY_USER}" --password-stdin "${HUB_REGISTRY}"
-        docker tag "${IMAGE}" "${HUB_IMAGE}"
-        docker push "${HUB_IMAGE}"
-        docker logout "${HUB_REGISTRY}"
-        set +e
-      fi
   except:
     - tags
     - merge_requests
@@ -192,3 +184,38 @@ ci-lemma-overloading-dev:
 ################
 ### deploy stage
 ################
+
+# Changes below (or jobs extending .docker-deploy) should be carefully
+# reviewed to avoid unwanted "token leaks"
+.docker-deploy:
+  stage: deploy
+  image: docker:latest
+  services:
+    - docker:dind
+  environment:
+    name: deployment
+    url: https://hub.docker.com/r/mathcomp/mathcomp-dev
+  variables:
+    HUB_IMAGE: "mathcomp/${CI_JOB_NAME}"
+    IMAGE_PREFIX: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}"
+  script:
+    - export IMAGE="${IMAGE_PREFIX}_${CI_JOB_NAME##*:}"
+    - docker pull "${IMAGE}"
+    - echo "${HUB_TOKEN}" | docker login -u "${HUB_REGISTRY_USER}" --password-stdin "${HUB_REGISTRY}"
+    - docker tag "${IMAGE}" "${HUB_IMAGE}"
+    - docker push "${HUB_IMAGE}"
+    - docker logout "${HUB_REGISTRY}"
+  only:
+    - master
+
+mathcomp-dev:coq-8.7:
+  extends: .docker-deploy
+
+mathcomp-dev:coq-8.8:
+  extends: .docker-deploy
+
+mathcomp-dev:coq-8.9:
+  extends: .docker-deploy
+
+mathcomp-dev:coq-dev:
+  extends: .docker-deploy