aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-22 12:05:06 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-22 12:05:06 +0200
commitad8eaffd5f65f20f91c186214ce2e3a755418ff8 (patch)
tree426485ca90eeb94239b2cafbef134e79d301504d /dev/ci
parente07f69ca60423a3fc5a0654bb7a24b2889d1a4c1 (diff)
parent3b089a920181aa6b6b959fc13ac86383f1c48198 (diff)
Merge PR #7526: [circle] Use Docker image from Gitlab registry.
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/README.md5
-rw-r--r--dev/ci/docker/README.md41
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile3
-rwxr-xr-xdev/ci/docker/bionic_coq/hooks/post_push8
4 files changed, 13 insertions, 44 deletions
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