aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-16 13:37:43 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-17 18:41:06 +0200
commit3b089a920181aa6b6b959fc13ac86383f1c48198 (patch)
tree0a85107948354611e35479dd985b78cdb8441041
parent5281317cb558f2b9aa6f854b9c7aeb617beba8e6 (diff)
[circle] Use Docker image from Gitlab registry.
-rw-r--r--.circleci/config.yml10
-rw-r--r--.gitlab-ci.yml2
-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
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