diff options
| -rw-r--r-- | .gitlab-ci.yml | 119 | ||||
| -rw-r--r-- | Dockerfile | 2 | ||||
| -rw-r--r-- | Dockerfile.make | 2 |
3 files changed, 86 insertions, 37 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index d0eabf4..d326aae 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: @@ -25,8 +26,37 @@ stages: - build + - deploy - test +################ +#### build stage +################ + +# set var OPAM_SWITCH (if need be) and COQ_VERSION when using +.make-build: + stage: build + image: docker:latest + services: + - docker:dind + 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}" . + except: + - tags + - merge_requests + +make-coq-latest: + extends: .make-build + variables: + COQ_VERSION: "latest" + # set var OPAM_SWITCH (if need be) when using .opam-build: stage: build @@ -35,23 +65,14 @@ stages: - 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 "${OPAM_SWITCH}" - echo "${CI_JOB_TOKEN}" | docker login -u "${CI_REGISTRY_USER}" --password-stdin "${CI_REGISTRY}" script: - 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 @@ -68,28 +89,10 @@ coq-8.9: coq-dev: extends: .opam-build -# set var OPAM_SWITCH (if need be) and COQ_VERSION when using -.make-build: - stage: build - image: docker:latest - services: - - docker:dind - variables: - # This image will be built locally only (not pushed) - IMAGE: "mathcomp-dev:make_coq-${COQ_VERSION}" - OPAM_SWITCH: "edge" - before_script: - script: - - docker build -f Dockerfile.make --pull --build-arg=coq_image="coqorg/coq:${COQ_VERSION}" --build-arg=compiler="${OPAM_SWITCH}" -t "${IMAGE}" . - except: - - tags - - merge_requests +################ +##### test stage +################ -make-coq-latest: - extends: .make-build - variables: - COQ_VERSION: "latest" - # set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using .ci: stage: test @@ -98,11 +101,14 @@ make-coq-latest: GIT_STRATEGY: none before_script: - cat /proc/{cpu,mem}info || true - # don't printenv if there are private tokens + # don't printenv to avoid cluttering the log - opam config list - opam repo list - opam list - coqc --version + - echo "${COQ_VERSION}" + - echo "${CONTRIB_URL}" + - echo "${CONTRIB_VERSION}" - git clone -b "${CONTRIB_VERSION}" --depth 1 "${CONTRIB_URL}" /home/coq/ci - cd /home/coq/ci - git rev-parse --verify HEAD @@ -180,3 +186,46 @@ ci-lemma-overloading-dev: extends: .ci-lemma-overloading variables: COQ_VERSION: "dev" + +################ +### deploy stage +################ + +# Changes below (or jobs extending .docker-deploy) should be carefully +# reviewed to avoid leaks of HUB_TOKEN +.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##*:}" + - echo "${IMAGE}" + - docker pull "${IMAGE}" + - echo "${HUB_IMAGE}" + - docker tag "${IMAGE}" "${HUB_IMAGE}" + - test -n "${HUB_REGISTRY}" + - test -n "${HUB_REGISTRY_USER}" + - echo "${HUB_TOKEN}" | docker login -u "${HUB_REGISTRY_USER}" --password-stdin "${HUB_REGISTRY}" + - 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 @@ -29,7 +29,7 @@ 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 -c -s --logs"] + && opam clean -a -s --logs"] FROM coqorg/base:bare diff --git a/Dockerfile.make b/Dockerfile.make index 4a3787d..7972ad7 100644 --- a/Dockerfile.make +++ b/Dockerfile.make @@ -21,7 +21,7 @@ RUN ["/bin/bash", "--login", "-c", "set -x \ && 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 -c -s --logs \ + && opam clean -a -s --logs \ && sudo chown -R coq:coq /home/coq/mathcomp \ && cd mathcomp \ && make Makefile.coq \ |