diff options
| author | Erik Martin-Dorel | 2020-03-08 15:22:33 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2020-03-08 15:51:14 +0100 |
| commit | 563f395e1a41caf4978fe9881250ec68796e36a0 (patch) | |
| tree | c26905760896e833863df5c20457f8af3b42b94b /.gitlab-ci.yml | |
| parent | a7f4eb76935157112aa844b6c5ac29a36898235f (diff) | |
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.
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 8 |
1 files changed, 2 insertions, 6 deletions
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 |