diff options
| -rw-r--r-- | .circleci/config.yml | 10 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | dev/ci/README.md | 5 | ||||
| -rw-r--r-- | dev/ci/docker/README.md | 41 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 3 | ||||
| -rwxr-xr-x | dev/ci/docker/bionic_coq/hooks/post_push | 8 |
6 files changed, 21 insertions, 48 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 79f83d472..4d2fb1a4d 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -8,10 +8,11 @@ defaults: # reference syntax) working_directory: ~/coq docker: - - image: coqci/base:V2018-05-07-V2 + - image: $CI_REGISTRY_IMAGE:$CACHEKEY environment: &envvars - NATIVE_COMP: "yes" + CACHEKEY: "bionic_coq-V2018-05-07-V2" + CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq version: 2 @@ -46,7 +47,9 @@ before_script: &before_script paths: - coq/ - environment: *envvars + environment: + <<: *envvars + NATIVE_COMP: "yes" .ci-template: &ci-template <<: *params @@ -63,6 +66,7 @@ before_script: &before_script root: *workspace paths: - coq/ + environment: *envvars # Defines individual jobs, see the workflows section below for job orchestration jobs: diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c010da4cf..07777441f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: bionic_coq-V2018-05-07-V2 + CACHEKEY: "bionic_coq-V2018-05-07-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/dev/ci/README.md b/dev/ci/README.md index dee3d2aff..ed3442e0d 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -141,7 +141,6 @@ no OCaml warnings build Coq in parallel with other tests. ### GitLab and Windows - If your repository has access to runners tagged `windows`, setting the secret variable `WINDOWS` to `enabled` will add jobs building Windows versions of Coq (32bit and 64bit). @@ -155,6 +154,10 @@ System and opam packages are installed in a Docker image. The image is automatically built and uploaded to your GitLab registry, and is loaded by subsequent jobs. +**IMPORTANT**: When updating Coq's CI docker image, you must modify +the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`, +and `Dockerfile`. + The Docker building job reuses the uploaded image if it is available, but if you wish to save more time you can skip the job by setting `SKIP_DOCKER` to `true`. diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md index 8e677f6f2..919e2a735 100644 --- a/dev/ci/docker/README.md +++ b/dev/ci/docker/README.md @@ -1,37 +1,13 @@ ## Overall Docker Setup for Coq's CI. This directory provides Docker images to be used by Coq's CI. The -images do support Docker autobuild on `hub.docker.com` +images do support Docker autobuild on `hub.docker.com` and Gitlab's +private registry. -Autobuild is the preferred build method [see below]; if you are a -member of the `coqci` organization, the automated build will push the -image to the `coqci/name:$VERSION` tag using a Docker hub hook. - -## Updating the Image and Syncronization with CI files - -Unfortunately, at this point some manual synchronization is needed -between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the -checklist is: - -- check the name and version of the image setup in `hooks/post_push` - have to match. -- check `COMPILER` variables do match. - -Once you are sure the variables are right, then proceed to trigger an -autobuild or do a manual build, et voilà ! - -## Docker Autobuilding. - -We provide basic support for auto-building, see: - -https://docs.docker.com/docker-cloud/builds/advanced/ - -If you are member of the `coqci` Docker organization, trigger an -autobuild in your account and the image will be pushed to it as we -set the proper tag in `hooks/post_push`. - -We still need to figure out how properly setup a more automated, -organization-wide auto-building process. +Gitlab CI will build and tag a Docker by default for every job if the +`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this +variable is usually set to `false` indeed to avoid booting a useless +job. ## Manual Building @@ -47,10 +23,6 @@ To upload/push to your hub: + `docker tag base:$VERSION $USER/base:$VERSION` + `docker push $USER/base:$VERSION` -Now your docker image is ready to be used. To upload to `coqci`: -- `docker tag base:$VERSION coqci/base:$VERSION` -- `docker push coqci/base:$VERSION` - ## Debugging / Misc To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>` @@ -62,4 +34,3 @@ end. ## Possible Improvements: - Use ARG for customizing versions, centralize variable setup; -- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry . diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 689d203a1..a1178ee2a 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,3 +1,6 @@ +# CACHEKEY: "bionic_coq-V2018-05-07-V2" +# ^^ Update when modifying this file. + FROM ubuntu:bionic LABEL maintainer="e@x80.org" diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push deleted file mode 100755 index 307680aa5..000000000 --- a/dev/ci/docker/bionic_coq/hooks/post_push +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -COQCI_VERSION=V2018-05-07-V2 -docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION -docker push $DOCKER_REPO:$COQCI_VERSION - -docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION -docker push coqci/base:$COQCI_VERSION |