diff options
| author | coqbot-app[bot] | 2020-11-28 16:19:04 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-28 16:19:04 +0000 |
| commit | 7514bc25c6e8dffeb58ae9af0916dac83953d337 (patch) | |
| tree | 20b47781f58ae602c113392ce233b085f39d46b0 | |
| parent | 16ebc1024bff1d4e0573079c660d9341f95c604e (diff) | |
| parent | ea795d144c59facfcfa1837fdce3ca654b159d58 (diff) | |
Merge PR #13487: CI: Use hash of dockerfile in CACHEKEY
Reviewed-by: Zimmi48
Reviewed-by: gares
| -rw-r--r-- | .gitlab-ci.yml | 7 | ||||
| -rw-r--r-- | dev/ci/README-developers.md | 2 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 3 | ||||
| -rwxr-xr-x | dev/lint-repository.sh | 3 | ||||
| -rwxr-xr-x | dev/tools/check-cachekey.sh | 10 |
5 files changed, 19 insertions, 6 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ddbace193a..bd015a40b6 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -17,9 +17,9 @@ stages: # some default values variables: - # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here - # for reference] - CACHEKEY: "bionic_coq-V2020-11-26-V92" + # Format: $IMAGE-V$DATE-$hash + # The $hash is the first 10 characters of the md5 of the dockerfile + CACHEKEY: "bionic_coq-V2020-11-26-db194d584e" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -59,6 +59,7 @@ before_script: - eval $(opam env) - opam list - opam config list + - dev/tools/check-cachekey.sh ################ GITLAB CACHING ###################### # - use artifacts between jobs # diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 801e29ac95..f5ca6c495f 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -171,7 +171,7 @@ loaded by subsequent jobs. **IMPORTANT**: When updating Coq's CI docker image, you must modify the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) -and [`Dockerfile`](docker/bionic_coq/Dockerfile) +(see comment near it for details). 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 diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 85107780f1..96d96328f8 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,5 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-11-26-V92" -# ^^ Update when modifying this file. +# Update CACHEKEY in the .gitlab-ci.yml when modifying this file. FROM ubuntu:bionic LABEL maintainer="e@x80.org" diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 7701264ad1..0bad2f4c62 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -32,4 +32,7 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 | echo Checking overlays dev/tools/check-overlays.sh || CODE=1 +echo Checking CACHEKEY +dev/tools/check-cachekey.sh || CODE=1 + exit $CODE diff --git a/dev/tools/check-cachekey.sh b/dev/tools/check-cachekey.sh new file mode 100755 index 0000000000..15e3fa93cb --- /dev/null +++ b/dev/tools/check-cachekey.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +hash=$(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10) +key=$(grep CACHEKEY: .gitlab-ci.yml) +keyhash=${key%\"} +keyhash=${keyhash##*-} +if ! [ "$hash" = "$keyhash" ]; then + echo "Bad CACHEKEY: expected '$hash' but got '$keyhash'" + exit 1 +fi |