From 563f395e1a41caf4978fe9881250ec68796e36a0 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 8 Mar 2020 15:22:33 +0100
Subject: refactor: Simplify the Dockerfiles

* the CLI option --build-arg=compiler="${OPAM_SWITCH}" is now useless
  (it had been introduced to be able to compile Coq versions < 8.7,
  while mathcomp-dev now requires Coq 8.7+)

* the "coqorg/base:bare" image now contains the two environment vars
  COMPILER and COMPILER_EDGE => clear COMPILER="" in mathcomp-dev's
  Dockerfile multi-stage build.
---
 .gitlab-ci.yml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to '.gitlab-ci.yml')

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2df217e..8be4087 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,7 +1,5 @@
 # Design:
 # - 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)")
 #   - 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.7)
@@ -43,12 +41,11 @@ stages:
   variables:
     # This image will be built locally only (not pushed)
     IMAGE: "mathcomp-dev:make_coq-${COQ_VERSION}"
-    OPAM_SWITCH: "edge"
   before_script:
     - echo "${OPAM_SWITCH}"
     - echo "${COQ_VERSION}"
   script:
-    - docker build -f Dockerfile.make --pull --build-arg=coq_image="coqorg/coq:${COQ_VERSION}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" .
+    - docker build -f Dockerfile.make --pull --build-arg=coq_image="coqorg/coq:${COQ_VERSION}" -t "${IMAGE}" .
   except:
     - tags
     - merge_requests
@@ -67,7 +64,6 @@ make-coq-latest:
     - docker:dind
   variables:
     IMAGE: "${CI_REGISTRY_IMAGE}:${CI_PIPELINE_IID}_${CI_COMMIT_REF_SLUG}_${CI_JOB_NAME}"
-    OPAM_SWITCH: "edge"
   before_script:
     - echo "${OPAM_SWITCH}"
     - echo "${CI_JOB_TOKEN}" | docker login -u "${CI_REGISTRY_USER}" --password-stdin "${CI_REGISTRY}"
@@ -85,7 +81,7 @@ make-coq-latest:
     - tags
     - merge_requests
     - schedules
-  
+
 coq-8.7:
   extends: .opam-build-once
 
-- 
cgit v1.2.3