Merge pull request #455 from erikmd/bump-opam

[ci] Simplify {Dockerfile,Dockerfile.make} & Restore the "opam clean -c" option

3 files changed, 13 insertions, 38 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 2df217e..930e9a4 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
 
@@ -225,16 +221,6 @@ ci-odd-order-dev:
     - opam pin add -n -k path coq-lemma-overloading .
     - opam install -y -v -j "${NJOBS}" coq-lemma-overloading
 
-ci-lemma-overloading-8.8:
-  extends: .ci-lemma-overloading
-  variables:
-    COQ_VERSION: "8.8"
-
-ci-lemma-overloading-8.9:
-  extends: .ci-lemma-overloading
-  variables:
-    COQ_VERSION: "8.9"
-
 ci-lemma-overloading-8.10:
   extends: .ci-lemma-overloading
   variables:
diff --git a/Dockerfile b/Dockerfile
index eddbb0f..65b7b30 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -5,18 +5,12 @@ WORKDIR /home/coq/mathcomp
 
 COPY . .
 
-ARG compiler="base"
-# other possible value: "edge"
-
 RUN ["/bin/bash", "--login", "-c", "set -x \
-  && declare -A switch_table \
-  && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \
-  && opam_switch=\"${switch_table[${compiler}]}\" \
-  && [ -n \"opam_switch\" ] \
-  && opam switch set ${opam_switch} \
+  && [ -n \"${COMPILER_EDGE}\" ] \
+  && opam switch set \"${COMPILER_EDGE}\" \
   && eval $(opam env) \
-  && unset \"switch_table[${compiler}]\" \
-  && for sw in \"${switch_table[@]}\"; do if [ -n \"$sw\" ]; then opam switch remove -y \"${sw}\"; fi; done \
+  && [ -n \"${COMPILER}\" ] \
+  && opam switch remove -y \"${COMPILER}\" \
   && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \
   && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \
   && opam update -y \
@@ -29,10 +23,11 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && opam pin add -n -k path coq-mathcomp-field . \
   && opam pin add -n -k path coq-mathcomp-character . \
   && opam install -y -v -j ${NJOBS} coq-mathcomp-character \
-  && opam clean -a -s --logs"]
+  && opam clean -a -c -s --logs"]
 
 FROM coqorg/base:bare
 
+ENV COMPILER=""
 ENV MATHCOMP_VERSION="dev"
 ENV MATHCOMP_PACKAGE="coq-mathcomp-character"
 
diff --git a/Dockerfile.make b/Dockerfile.make
index 1a1dfc2..8f305ae 100644
--- a/Dockerfile.make
+++ b/Dockerfile.make
@@ -5,23 +5,17 @@ WORKDIR /home/coq/mathcomp
 
 COPY . .
 
-ARG compiler="base"
-# other possible value: "edge"
-
 RUN ["/bin/bash", "--login", "-c", "set -x \
-  && declare -A switch_table \
-  && switch_table=( [\"base\"]=\"${COMPILER}\" [\"edge\"]=\"${COMPILER_EDGE}\" ) \
-  && opam_switch=\"${switch_table[${compiler}]}\" \
-  && [ -n \"opam_switch\" ] \
-  && opam switch set ${opam_switch} \
+  && [ -n \"${COMPILER_EDGE}\" ] \
+  && opam switch set \"${COMPILER_EDGE}\" \
   && eval $(opam env) \
-  && unset \"switch_table[${compiler}]\" \
-  && for sw in \"${switch_table[@]}\"; do [ -n \"$sw\" ] && opam switch remove -y \"${sw}\"; done \
+  && [ -n \"${COMPILER}\" ] \
+  && opam switch remove -y \"${COMPILER}\" \
   && opam repository add --all-switches --set-default coq-extra-dev https://coq.inria.fr/opam/extra-dev \
   && opam repository add --all-switches --set-default coq-core-dev https://coq.inria.fr/opam/core-dev \
   && opam update -y \
   && opam config list && opam repo list && opam list && coqc --version \
-  && opam clean -a -s --logs \
+  && opam clean -a -c -s --logs \
   && sudo chown -R coq:coq /home/coq/mathcomp \
   && cd mathcomp \
   && make Makefile.coq \