From f3ef7928b2d92a93ad9da28bb703ba4a5e715880 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 5 May 2018 13:14:10 +0200
Subject: Gitlab: build docker image in pipeline and use through registry.

A docker-boot job is added which builds the docker image and pushes it
to the registry, the other jobs running on the image from the
registry.

The boot job reuses the already pushed image if it exists and matches,
this is important to cut down its runtime.

Making a new image takes 30min for all the switches
https://gitlab.com/SkySkimmer/coq/-/jobs/66650546
For testing I removed all jobs except boot and main build, and after
that run I built only the standard switch.

Building 1 switch takes around 20min
https://gitlab.com/SkySkimmer/coq/-/jobs/66656942
When the registry is up to date it takes 2min
https://gitlab.com/SkySkimmer/coq/-/jobs/66658790
(I don't know about all switches but probably no more than 5min)

Each pipeline pushes the image to $CI_REGISTRY_IMAGE:$CI_PIPELINE_ID
which is eg registry.gitlab.com/skyskimmer/coq:21557176 and is what
the other jobs use to run themselves.

For caching it pulls from and pushes to a constant name, in this test
$CI_REGISTRY_IMAGE:$CACHEKEY. We might also want to pull from the main
coq repo to avoid redoing work.

The question of having 1 image or 1 image/switch remains open.

Using the gitlab registry doesn't really work for circle CI, so the
dockerhub account would have to remain (or circle could return to an
opam-boot job, or be removed from our CI). There are similar concerns
with travis if we want to move it to docker.
---
 .gitlab-ci.yml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 095099690b..3ef592abc3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,6 +1,7 @@
-image: coqci/base:V2018-05-07-V2
+image: "$IMAGE"
 
 stages:
+  - docker
   - build
   - test
 
@@ -9,11 +10,25 @@ variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
   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"
   # Used to select special compiler switches such as flambda, 32bits, etc...
   OPAM_VARIANT: ""
 
+docker-boot:
+  stage: docker
+  image: docker:stable
+  services:
+    - docker:dind
+  before_script: []
+  script:
+    - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
+    - cd dev/ci/docker/bionic_coq/
+    - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
+    - docker build -t "$IMAGE" .
+    - docker push "$IMAGE"
+
 before_script:
   - cat /proc/{cpu,mem}info || true
   - ls -a # figure out if artifacts are around
-- 
cgit v1.2.3


From 413bb2cf6a2eafd06e9ae1da7dcec749ab6f227b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 14 May 2018 14:04:16 +0200
Subject: Gitlab: skip docker job when $SKIP_DOCKER == "true".

---
 .gitlab-ci.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3ef592abc3..3d4cee8fbc 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -28,6 +28,9 @@ docker-boot:
     - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
     - docker build -t "$IMAGE" .
     - docker push "$IMAGE"
+  except:
+    variables:
+      - $SKIP_DOCKER == "true"
 
 before_script:
   - cat /proc/{cpu,mem}info || true
-- 
cgit v1.2.3


From fb4d41ff88b7a339db2e40ea96738e0da50f65ee Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 14 May 2018 15:51:00 +0200
Subject: Update CI README with info about gitlab windows and docker jobs.

---
 dev/ci/README.md | 27 ++++++++++++++++++++++++++-
 1 file changed, 26 insertions(+), 1 deletion(-)

diff --git a/dev/ci/README.md b/dev/ci/README.md
index 87f03aa994..dee3d2aff7 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -96,7 +96,8 @@ PR by running GitLab CI on your private branches. To do so follow these steps:
 2. Click on "New Project".
 3. Choose "CI / CD for external repository" then click on "GitHub".
 4. Find your fork of the Coq repository and click on "Connect".
-5. You are encouraged to go to the CI / CD general settings and increase the
+5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project).
+6. You are encouraged to go to the CI / CD general settings and increase the
    timeout from 1h to 2h for better reliability.
 
 Now everytime you push (including force-push unless you changed the default
@@ -137,3 +138,27 @@ Currently, available artifacts are:
 
 As an exception to the above, jobs testing that compilation triggers
 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).
+
+The Windows jobs are enabled on Coq's repository, where pipelines for
+pull requests run.
+
+### GitLab and Docker
+
+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.
+
+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`.
+
+This means you will need to change its value when the Docker image
+needs to be updated. You can do so for a single pipeline by starting
+it through the web interface.
-- 
cgit v1.2.3