From d7178c4fb6a2bf0f995ea237724ca7820036b81e Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 3 Jul 2020 17:05:45 +0200 Subject: [PATCH 1/9] feat: Switch to single-switch images Close coq-community/docker-coq#4 --- coq/beta/Dockerfile | 1 - coq/dev/Dockerfile | 1 - coq/dual/beta/Dockerfile | 1 - coq/dual/dev/Dockerfile | 1 - coq/dual/stable/Dockerfile | 1 - coq/stable/Dockerfile | 1 - images.yml | 149 ++++++++++++++----------------------- 7 files changed, 57 insertions(+), 98 deletions(-) diff --git a/coq/beta/Dockerfile b/coq/beta/Dockerfile index 678ba38..c9dde31 100644 --- a/coq/beta/Dockerfile +++ b/coq/beta/Dockerfile @@ -1,4 +1,3 @@ -# TODO later: Use coqorg/base:4.05.0 ARG BASE_TAG="latest" FROM coqorg/base:${BASE_TAG} diff --git a/coq/dev/Dockerfile b/coq/dev/Dockerfile index 2b6a76f..1c50da6 100644 --- a/coq/dev/Dockerfile +++ b/coq/dev/Dockerfile @@ -1,4 +1,3 @@ -# TODO later: Use coqorg/base:4.05.0 ARG BASE_TAG="latest" FROM coqorg/base:${BASE_TAG} diff --git a/coq/dual/beta/Dockerfile b/coq/dual/beta/Dockerfile index 4f7dde3..225f9df 100644 --- a/coq/dual/beta/Dockerfile +++ b/coq/dual/beta/Dockerfile @@ -1,4 +1,3 @@ -# TODO later: Use coqorg/base:4.05.0 ARG BASE_TAG="latest" FROM coqorg/base:${BASE_TAG} diff --git a/coq/dual/dev/Dockerfile b/coq/dual/dev/Dockerfile index a1e39b8..b3b30c7 100644 --- a/coq/dual/dev/Dockerfile +++ b/coq/dual/dev/Dockerfile @@ -1,4 +1,3 @@ -# TODO later: Use coqorg/base:4.05.0 ARG BASE_TAG="latest" FROM coqorg/base:${BASE_TAG} diff --git a/coq/dual/stable/Dockerfile b/coq/dual/stable/Dockerfile index 397b440..41dd2cd 100644 --- a/coq/dual/stable/Dockerfile +++ b/coq/dual/stable/Dockerfile @@ -1,4 +1,3 @@ -# TODO later: Use coqorg/base:4.05.0 ARG BASE_TAG="latest" FROM coqorg/base:${BASE_TAG} diff --git a/coq/stable/Dockerfile b/coq/stable/Dockerfile index 86fcaf6..7c32449 100644 --- a/coq/stable/Dockerfile +++ b/coq/stable/Dockerfile @@ -1,4 +1,3 @@ -# TODO later: Use coqorg/base:4.05.0 ARG BASE_TAG="latest" FROM coqorg/base:${BASE_TAG} diff --git a/images.yml b/images.yml index 8a735d8..8430a31 100644 --- a/images.yml +++ b/images.yml @@ -6,30 +6,8 @@ args: BUILD_DATE: '{defaults[build_date]}' images: - matrix: - # TODO: replace latest with 2 images (single-switch), merge tags - base: ['latest'] - coq: ['dev'] - build: - keywords: - - 'dev' - context: './coq' - dockerfile: './dual/dev/Dockerfile' - commit_api: - fetcher: 'github' - repo: 'coq/coq' - branch: 'master' - args: - BASE_TAG: '{matrix[base]}' - COQ_VERSION: '{matrix[coq]}' - COQ_COMMIT: '{defaults[commit]}' - VCS_REF: '{defaults[commit][0:7]}' - COQ_EXTRA_OPAM: 'coq-bignums' - tags: - - tag: '{matrix[coq]}' - if: '{matrix[base]} == "latest"' - # TODO: remove all occurrences of 'coqorg/base:latest' - - matrix: - base: ['4.09.1-flambda'] + minimal: ['4.05.0'] + base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] coq: ['dev'] build: keywords: @@ -47,91 +25,85 @@ images: VCS_REF: '{defaults[commit][0:7]}' COQ_EXTRA_OPAM: 'coq-bignums' tags: + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[minimal]}' - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - if: '{matrix[base]} != "latest"' + if: '{matrix[base]} != {matrix[minimal]}' - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*-*]}-flambda' - if: '{matrix[base]} != "latest"' - # TODO/FIXME: Update later on + if: '{matrix[base]} != {matrix[minimal]}' + # TODO: Uncomment when the v8.14 branch is created # - matrix: - # base: ['latest', '4.09.1-flambda'] + # minimal: ['4.05.0'] + # base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] + # # TODO: Update when appropriate # coq: ['8.14-alpha'] # build: - # keywords: - # - '{matrix[coq][%-*]}' - # context: './coq' - # dockerfile: './dev/Dockerfile' + # # TODO: Remove this commit_api section when the beta is released # commit_api: # fetcher: 'github' # repo: 'coq/coq' # branch: 'v8.14' + # context: './coq' + # # TODO: Replace with "beta/Dockerfile" when the beta is released + # dockerfile: './dev/Dockerfile' + # keywords: + # - '{matrix[coq][%-*]}' # args: # BASE_TAG: '{matrix[base]}' + # # TODO: Replace with '{matrix[coq]}' when the beta is released # COQ_VERSION: '{matrix[coq][%-*]}.dev' # COQ_COMMIT: '{defaults[commit]}' + # # TODO: Replace with 'V{matrix[coq][//-/+]}' when the beta is released # VCS_REF: '{defaults[commit][0:7]}' # COQ_EXTRA_OPAM: 'coq-bignums' # tags: # - tag: '{matrix[coq]}' - # if: '{matrix[base]} == "latest"' - # - tag: '{matrix[coq][%-*]}' - # if: '{matrix[base]} == "latest"' + # if: '{matrix[base]} == {matrix[minimal]}' # - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - # if: '{matrix[base]} != "latest"' + # if: '{matrix[base]} != {matrix[minimal]}' # - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*-*]}-flambda' - # if: '{matrix[base]} != "latest"' + # if: '{matrix[base]} != {matrix[minimal]}' - matrix: - base: ['latest'] + minimal: ['4.05.0'] + base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] + # TODO: Update when appropriate coq: ['8.13-alpha'] build: - keywords: - - '8.13' - context: './coq' - dockerfile: './dual/dev/Dockerfile' + # TODO: Remove this commit_api section when the beta is released commit_api: fetcher: 'github' repo: 'coq/coq' branch: 'v8.13' - args: - BASE_TAG: '{matrix[base]}' - COQ_VERSION: '{matrix[coq][%-*]}.dev' - COQ_COMMIT: '{defaults[commit]}' - VCS_REF: '{defaults[commit][0:7]}' - COQ_EXTRA_OPAM: 'coq-bignums' - tags: - - tag: '{matrix[coq]}' - if: '{matrix[base]} == "latest"' - - tag: '{matrix[coq][%-*]}' - if: '{matrix[base]} == "latest"' - - matrix: - base: ['4.09.1-flambda'] - coq: ['8.13-alpha'] - build: - keywords: - - '8.13' context: './coq' + # TODO: Replace with "beta/Dockerfile" when the beta is released dockerfile: './dev/Dockerfile' - commit_api: - fetcher: 'github' - repo: 'coq/coq' - branch: 'v8.13' + keywords: + - '8.13' args: BASE_TAG: '{matrix[base]}' + # TODO: Replace with '{matrix[coq]}' when the beta is released COQ_VERSION: '{matrix[coq][%-*]}.dev' COQ_COMMIT: '{defaults[commit]}' + # TODO: Replace with 'V{matrix[coq][//-/+]}' when the beta is released VCS_REF: '{defaults[commit][0:7]}' COQ_EXTRA_OPAM: 'coq-bignums' tags: + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[minimal]}' + - tag: '{matrix[coq][%-*]}' + if: '{matrix[base]} == {matrix[minimal]}' - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - if: '{matrix[base]} != "latest"' + if: '{matrix[base]} != {matrix[minimal]}' - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*-*]}-flambda' - if: '{matrix[base]} != "latest"' + if: '{matrix[base]} != {matrix[minimal]}' - matrix: - # TODO: replace latest with 2 images (single-switch), merge tags - base: ['latest'] + minimal: ['4.05.0'] + base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] coq: ['8.12.1', '8.11.2', '8.10.2', '8.9.1', '8.8.2'] + coq_latest: ['8.12.1'] build: context: './coq' - dockerfile: './dual/stable/Dockerfile' + dockerfile: './stable/Dockerfile' args: BASE_TAG: '{matrix[base]}' COQ_VERSION: '{matrix[coq]}' @@ -140,40 +112,27 @@ images: tags: - tag: 'latest' if: - # TODO: Bump this version too: - - '{matrix[coq]} == "8.12.1"' - - '{matrix[base]} == "latest"' + - '{matrix[coq]} == {matrix[coq_latest]}' + - '{matrix[base]} == {matrix[minimal]}' - tag: '{matrix[coq]}' - if: '{matrix[base]} == "latest"' + if: '{matrix[base]} == {matrix[minimal]}' - tag: '{matrix[coq][%.*]}' - if: '{matrix[base]} == "latest"' - - matrix: - base: ['4.09.1-flambda'] - coq: ['8.12.1', '8.11.2', '8.10.2', '8.9.1', '8.8.2'] - build: - context: './coq' - dockerfile: './stable/Dockerfile' - args: - BASE_TAG: '{matrix[base]}' - COQ_VERSION: '{matrix[coq]}' - VCS_REF: 'V{matrix[coq]}' - COQ_EXTRA_OPAM: 'coq-bignums' - tags: + if: '{matrix[base]} == {matrix[minimal]}' - tag: 'latest-ocaml-{matrix[base][%.*-*]}-flambda' if: - # TODO: Bump this version too: - - '{matrix[coq]} == "8.12.1"' - - '{matrix[base]} != "latest"' + - '{matrix[coq]} == {matrix[coq_latest]}' + - '{matrix[base]} != {matrix[minimal]}' - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - if: '{matrix[base]} != "latest"' + if: '{matrix[base]} != {matrix[minimal]}' - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda' - if: '{matrix[base]} != "latest"' + if: '{matrix[base]} != {matrix[minimal]}' - matrix: - base: ['latest'] + minimal: ['4.05.0'] + base: ['4.05.0', '4.07.1-flambda'] coq: ['8.7.2'] build: context: './coq' - dockerfile: './dual/stable/Dockerfile' + dockerfile: './stable/Dockerfile' args: BASE_TAG: '{matrix[base]}' COQ_VERSION: '{matrix[coq]}' @@ -181,7 +140,13 @@ images: COQ_EXTRA_OPAM: 'coq-bignums' tags: - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[minimal]}' - tag: '{matrix[coq][%.*]}' + if: '{matrix[base]} == {matrix[minimal]}' + - tag: '{matrix[coq]}-ocaml-{matrix[base]}' + if: '{matrix[base]} != {matrix[minimal]}' + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda' + if: '{matrix[base]} != {matrix[minimal]}' - matrix: base: ['4.02.3'] coq: ['8.6.1'] From f530f6489fe0b0a176fdc6e748bf8449fa366538 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 6 Dec 2020 02:56:05 +0100 Subject: [PATCH 2/9] feat: Add admin.sh (helper functions to compute compatible OCaml versions) --- admin.sh | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 admin.sh diff --git a/admin.sh b/admin.sh new file mode 100644 index 0000000..0909eaa --- /dev/null +++ b/admin.sh @@ -0,0 +1,63 @@ +#!/usr/bin/env bash +# Author: Erik Martin-Dorel, 2020 +# Summary: helper functions to compute compatible OCaml versions + +ocamls() { opam switch list-available ocaml-base-compiler | grep -v -e '#' | cut -d ' ' -f 2; } + +pred_ocaml_for_coqs() { + for v; do + printf "* Coq $v: "'`' + printf '%s' "$(opam show "coq.$v" -f depends: | grep '"ocaml"')" + printf '`\n' + done +} + +list_ocaml_for_coqs() { + local indent=' ' + # To change manually: + local render='true' + # local render='false' + # Note: we may post-process the output to merge "coq" items with same ocaml + for v; do + local several='true' + printf "* Coq $v: " + if [ "$v" = "8.4.6" ] || [ "$v" = "8.5.3" ] || [ "$v" = "8.6.1" ]; then + minimal="4.02.3" + several='false' + else + versions=$(opam search ocaml-base-compiler --no-switch --columns=version -V --coinstallable-with="coq.$v" | grep -v -e '#') + if [[ "$versions" =~ "4.05.0" ]]; then + minimal="4.05.0" + else + minimal=$(head -n 1 <<<"$versions") + fi + fi + [ "$render" = 'true' ] && printf "\n${indent}minimal: ['" + printf "$minimal" + [ "$render" = 'true' ] && printf "']\n" + [ "$render" = 'true' ] && printf "${indent}base: ['$minimal'" + if [ "$several" = 'true' ]; then + if [[ "$versions" =~ "4.07.1" ]]; then + if [ "$render" = 'true' ]; then + printf ", '4.07.1-flambda'" + else + printf " 4.07.1-flambda" + fi + fi + minor=$(cut -d '.' -f 1-2 <<<"$versions" | sort -u -V | tail -n 2) + lasttwo=$(for v in $minor; do grep -e "^${v//./\\.}.*\$" <<<"$versions" | tail -n 1; done) + maybelasttwo=$(grep -v -e "^${minimal//./\\.}\$" -e '^4\.07$' <<<"$lasttwo") + if [ "$render" = 'true' ]; then + printf '%s' "$maybelasttwo" | xargs printf ", '%s-flambda'" + else + printf '%s' "$maybelasttwo" | xargs printf " %s-flambda" + fi + fi + [ "$render" = 'true' ] && printf "]" + printf "\n" + [ "$render" = 'true' ] && printf "${indent}coq: ['${v}']\n" + done +} + +# pred_ocaml_for_coqs 8.4.6 8.5.3 8.6.1 8.7.2 8.8.2 8.9.1 8.10.2 8.11.2 8.12.1 # 8.13-alpha +# list_ocaml_for_coqs 8.13.dev 8.12.1 8.11.2 8.10.2 8.9.1 8.8.2 8.7.2 8.6.1 8.5.3 8.4.6 From ea05ffb8ed1e852b1cd4ab22ebf67f14dac2cf0e Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 6 Dec 2020 03:11:02 +0100 Subject: [PATCH 3/9] feat: Apply the ocaml-version policy discussed in issue #12 href: https://github.com/coq-community/docker-coq/issues/12#issuecomment-707165691 --- images.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/images.yml b/images.yml index 8430a31..f6db01c 100644 --- a/images.yml +++ b/images.yml @@ -7,7 +7,7 @@ args: images: - matrix: minimal: ['4.05.0'] - base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] + base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] coq: ['dev'] build: keywords: @@ -65,7 +65,7 @@ images: # if: '{matrix[base]} != {matrix[minimal]}' - matrix: minimal: ['4.05.0'] - base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] + base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] # TODO: Update when appropriate coq: ['8.13-alpha'] build: @@ -98,8 +98,8 @@ images: if: '{matrix[base]} != {matrix[minimal]}' - matrix: minimal: ['4.05.0'] - base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] - coq: ['8.12.1', '8.11.2', '8.10.2', '8.9.1', '8.8.2'] + base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] + coq: ['8.12.1', '8.11.2'] coq_latest: ['8.12.1'] build: context: './coq' @@ -128,8 +128,8 @@ images: if: '{matrix[base]} != {matrix[minimal]}' - matrix: minimal: ['4.05.0'] - base: ['4.05.0', '4.07.1-flambda'] - coq: ['8.7.2'] + base: ['4.05.0', '4.07.1-flambda', '4.08.1-flambda', '4.09.1-flambda'] + coq: ['8.10.2', '8.9.1', '8.8.2', '8.7.2'] build: context: './coq' dockerfile: './stable/Dockerfile' From 4da77c31621b9ff6f2991f1bbc5ae1e8ce5e8c09 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 7 Dec 2020 09:02:27 +0100 Subject: [PATCH 4/9] refactor: s/minimal:/default:/ --- admin.sh | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/admin.sh b/admin.sh index 0909eaa..92a804a 100644 --- a/admin.sh +++ b/admin.sh @@ -23,6 +23,7 @@ list_ocaml_for_coqs() { printf "* Coq $v: " if [ "$v" = "8.4.6" ] || [ "$v" = "8.5.3" ] || [ "$v" = "8.6.1" ]; then minimal="4.02.3" + default="4.02.3" several='false' else versions=$(opam search ocaml-base-compiler --no-switch --columns=version -V --coinstallable-with="coq.$v" | grep -v -e '#') @@ -31,9 +32,18 @@ list_ocaml_for_coqs() { else minimal=$(head -n 1 <<<"$versions") fi + if [[ "$versions" =~ "4.07.1" ]]; then + default="4.07.1-flambda" + else + default="$minimal" + fi + fi + [ "$render" = 'true' ] && printf "\n${indent}default: ['" + if [ "$render" = 'true' ]; then + printf "$default" + else + printf "$minimal" fi - [ "$render" = 'true' ] && printf "\n${indent}minimal: ['" - printf "$minimal" [ "$render" = 'true' ] && printf "']\n" [ "$render" = 'true' ] && printf "${indent}base: ['$minimal'" if [ "$several" = 'true' ]; then From 03f379b23bbff026ae980545dfb2f8b2dae60730 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 7 Dec 2020 09:36:37 +0100 Subject: [PATCH 5/9] feat: Update the tags naming convention further, following #12 --- images.yml | 91 +++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 63 insertions(+), 28 deletions(-) diff --git a/images.yml b/images.yml index f6db01c..a472d9c 100644 --- a/images.yml +++ b/images.yml @@ -6,7 +6,7 @@ args: BUILD_DATE: '{defaults[build_date]}' images: - matrix: - minimal: ['4.05.0'] + default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] coq: ['dev'] build: @@ -25,15 +25,20 @@ images: VCS_REF: '{defaults[commit][0:7]}' COQ_EXTRA_OPAM: 'coq-bignums' tags: + # default tag (dev) - tag: '{matrix[coq]}' - if: '{matrix[base]} == {matrix[minimal]}' + if: '{matrix[base]} == {matrix[default]}' + # full tag - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - if: '{matrix[base]} != {matrix[minimal]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*-*]}-flambda' - if: '{matrix[base]} != {matrix[minimal]}' + if: '{matrix[base]} != 4.05.0' # TODO: Uncomment when the v8.14 branch is created # - matrix: - # minimal: ['4.05.0'] + # default: ['4.07.1-flambda'] # base: ['4.05.0', '4.07.1-flambda', '4.09.1-flambda'] # # TODO: Update when appropriate # coq: ['8.14-alpha'] @@ -57,14 +62,19 @@ images: # VCS_REF: '{defaults[commit][0:7]}' # COQ_EXTRA_OPAM: 'coq-bignums' # tags: + # # default tag (dev) # - tag: '{matrix[coq]}' - # if: '{matrix[base]} == {matrix[minimal]}' + # if: '{matrix[base]} == {matrix[default]}' + # # full tag # - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - # if: '{matrix[base]} != {matrix[minimal]}' - # - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*-*]}-flambda' - # if: '{matrix[base]} != {matrix[minimal]}' + # # abbreviated tag (*-ocaml-4.05) + # - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*]}' + # if: '{matrix[base]} == 4.05.0' + # # abbreviated tag (*-ocaml-4.07-flambda) + # - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*-*]}-flambda' + # if: '{matrix[base]} != 4.05.0' - matrix: - minimal: ['4.05.0'] + default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] # TODO: Update when appropriate coq: ['8.13-alpha'] @@ -88,16 +98,22 @@ images: VCS_REF: '{defaults[commit][0:7]}' COQ_EXTRA_OPAM: 'coq-bignums' tags: + # default tag (8.13-alpha) - tag: '{matrix[coq]}' - if: '{matrix[base]} == {matrix[minimal]}' + if: '{matrix[base]} == {matrix[default]}' + # abbreviated tag (8.13) - tag: '{matrix[coq][%-*]}' - if: '{matrix[base]} == {matrix[minimal]}' + if: '{matrix[base]} == {matrix[default]}' + # full tag - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - if: '{matrix[base]} != {matrix[minimal]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*-*]}-flambda' - if: '{matrix[base]} != {matrix[minimal]}' + if: '{matrix[base]} != 4.05.0' - matrix: - minimal: ['4.05.0'] + default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] coq: ['8.12.1', '8.11.2'] coq_latest: ['8.12.1'] @@ -110,24 +126,37 @@ images: VCS_REF: 'V{matrix[coq]}' COQ_EXTRA_OPAM: 'coq-bignums' tags: + # latest tag - tag: 'latest' if: - '{matrix[coq]} == {matrix[coq_latest]}' - - '{matrix[base]} == {matrix[minimal]}' - - tag: '{matrix[coq]}' - if: '{matrix[base]} == {matrix[minimal]}' - - tag: '{matrix[coq][%.*]}' - if: '{matrix[base]} == {matrix[minimal]}' + - '{matrix[base]} == {matrix[default]}' + # latest-abbreviated tag (*-ocaml-4.05) + - tag: 'latest-ocaml-{matrix[base][%.*]}' + if: + - '{matrix[coq]} == {matrix[coq_latest]}' + - '{matrix[base]} == 4.05.0' + # latest-abbreviated tag (*-ocaml-4.07-flambda) - tag: 'latest-ocaml-{matrix[base][%.*-*]}-flambda' if: - '{matrix[coq]} == {matrix[coq_latest]}' - - '{matrix[base]} != {matrix[minimal]}' + - '{matrix[base]} != 4.05.0' + # default tag (8.12.1) + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[default]}' + # abbreviated tag (8.12) + - tag: '{matrix[coq][%.*]}' + if: '{matrix[base]} == {matrix[default]}' + # full tag - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - if: '{matrix[base]} != {matrix[minimal]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda' - if: '{matrix[base]} != {matrix[minimal]}' + if: '{matrix[base]} != 4.05.0' - matrix: - minimal: ['4.05.0'] + default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.08.1-flambda', '4.09.1-flambda'] coq: ['8.10.2', '8.9.1', '8.8.2', '8.7.2'] build: @@ -139,14 +168,20 @@ images: VCS_REF: 'V{matrix[coq]}' COQ_EXTRA_OPAM: 'coq-bignums' tags: + # default tag (8.10.2) - tag: '{matrix[coq]}' - if: '{matrix[base]} == {matrix[minimal]}' + if: '{matrix[base]} == {matrix[default]}' + # abbreviated tag (8.10) - tag: '{matrix[coq][%.*]}' - if: '{matrix[base]} == {matrix[minimal]}' + if: '{matrix[base]} == {matrix[default]}' + # full tag - tag: '{matrix[coq]}-ocaml-{matrix[base]}' - if: '{matrix[base]} != {matrix[minimal]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda' - if: '{matrix[base]} != {matrix[minimal]}' + if: '{matrix[base]} != 4.05.0' - matrix: base: ['4.02.3'] coq: ['8.6.1'] From ebce9158ff9539da5cc5d23a8c6ebe74b8ca1a1a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 7 Dec 2020 11:47:41 +0100 Subject: [PATCH 6/9] fix: Don't forget OCaml 4.02.3 --- images.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/images.yml b/images.yml index a472d9c..814300c 100644 --- a/images.yml +++ b/images.yml @@ -196,6 +196,8 @@ images: tags: - tag: '{matrix[coq]}' - tag: '{matrix[coq][%.*]}' + - tag: '{matrix[coq]}-ocaml-{matrix[base]}' + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*]}' - matrix: base: ['4.02.3'] coq: ['8.5pl3', '8.4pl6'] @@ -210,3 +212,5 @@ images: tags: - tag: '{matrix[coq][//pl/.]}' - tag: '{matrix[coq][//pl/.][%.*]}' + - tag: '{matrix[coq][//pl/.]}-ocaml-{matrix[base]}' + - tag: '{matrix[coq][//pl/.][%.*]}-ocaml-{matrix[base][%.*]}' From 80f99f992a1a72124a1924a25d0a612dd3f8eb7d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 7 Dec 2020 09:41:38 +0100 Subject: [PATCH 7/9] refactor: Re-order the tags for latest-* --- images.yml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/images.yml b/images.yml index 814300c..5f80b36 100644 --- a/images.yml +++ b/images.yml @@ -131,6 +131,12 @@ images: if: - '{matrix[coq]} == {matrix[coq_latest]}' - '{matrix[base]} == {matrix[default]}' + # default tag (8.12.1) + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[default]}' + # abbreviated tag (8.12) + - tag: '{matrix[coq][%.*]}' + if: '{matrix[base]} == {matrix[default]}' # latest-abbreviated tag (*-ocaml-4.05) - tag: 'latest-ocaml-{matrix[base][%.*]}' if: @@ -141,12 +147,6 @@ images: if: - '{matrix[coq]} == {matrix[coq_latest]}' - '{matrix[base]} != 4.05.0' - # default tag (8.12.1) - - tag: '{matrix[coq]}' - if: '{matrix[base]} == {matrix[default]}' - # abbreviated tag (8.12) - - tag: '{matrix[coq][%.*]}' - if: '{matrix[base]} == {matrix[default]}' # full tag - tag: '{matrix[coq]}-ocaml-{matrix[base]}' # abbreviated tag (*-ocaml-4.05) From 0ca473b52006a99490338a64198dd6aab9afe7ac Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 7 Dec 2020 10:23:24 +0100 Subject: [PATCH 8/9] feat: Install the coq-native package --- images.yml | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/images.yml b/images.yml index 5f80b36..c87401f 100644 --- a/images.yml +++ b/images.yml @@ -23,7 +23,7 @@ images: COQ_VERSION: '{matrix[coq]}' COQ_COMMIT: '{defaults[commit]}' VCS_REF: '{defaults[commit][0:7]}' - COQ_EXTRA_OPAM: 'coq-bignums' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' tags: # default tag (dev) - tag: '{matrix[coq]}' @@ -60,7 +60,7 @@ images: # COQ_COMMIT: '{defaults[commit]}' # # TODO: Replace with 'V{matrix[coq][//-/+]}' when the beta is released # VCS_REF: '{defaults[commit][0:7]}' - # COQ_EXTRA_OPAM: 'coq-bignums' + # COQ_EXTRA_OPAM: 'coq-native coq-bignums' # tags: # # default tag (dev) # - tag: '{matrix[coq]}' @@ -96,7 +96,7 @@ images: COQ_COMMIT: '{defaults[commit]}' # TODO: Replace with 'V{matrix[coq][//-/+]}' when the beta is released VCS_REF: '{defaults[commit][0:7]}' - COQ_EXTRA_OPAM: 'coq-bignums' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' tags: # default tag (8.13-alpha) - tag: '{matrix[coq]}' @@ -124,7 +124,7 @@ images: BASE_TAG: '{matrix[base]}' COQ_VERSION: '{matrix[coq]}' VCS_REF: 'V{matrix[coq]}' - COQ_EXTRA_OPAM: 'coq-bignums' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' tags: # latest tag - tag: 'latest' @@ -166,7 +166,7 @@ images: BASE_TAG: '{matrix[base]}' COQ_VERSION: '{matrix[coq]}' VCS_REF: 'V{matrix[coq]}' - COQ_EXTRA_OPAM: 'coq-bignums' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' tags: # default tag (8.10.2) - tag: '{matrix[coq]}' @@ -192,7 +192,7 @@ images: BASE_TAG: '{matrix[base]}' COQ_VERSION: '{matrix[coq]}' VCS_REF: 'V{matrix[coq]}' - COQ_EXTRA_OPAM: 'coq-bignums' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' tags: - tag: '{matrix[coq]}' - tag: '{matrix[coq][%.*]}' @@ -200,7 +200,21 @@ images: - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*]}' - matrix: base: ['4.02.3'] - coq: ['8.5pl3', '8.4pl6'] + coq: ['8.5pl3'] + build: + context: './coq' + dockerfile: './stable/Dockerfile' + args: + BASE_TAG: '{matrix[base]}' + COQ_VERSION: '{matrix[coq][//pl/.]}' + VCS_REF: 'V{matrix[coq]}' + COQ_EXTRA_OPAM: 'coq-native' + tags: + - tag: '{matrix[coq][//pl/.]}' + - tag: '{matrix[coq][//pl/.][%.*]}' + - matrix: + base: ['4.02.3'] + coq: ['8.4pl6'] build: context: './coq' dockerfile: './stable/Dockerfile' From ceb9214c3044ec8209a01a0f7604ef2a58b80729 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 7 Dec 2020 10:50:06 +0100 Subject: [PATCH 9/9] feat: Update images.yml to setup a migration phase to single-switch (regarding "default" tags coqorg/coq:$COQ_VERSION) --- images.yml | 160 +++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 156 insertions(+), 4 deletions(-) diff --git a/images.yml b/images.yml index c87401f..453a515 100644 --- a/images.yml +++ b/images.yml @@ -5,8 +5,42 @@ docker_repo: 'coqorg/coq' args: BUILD_DATE: '{defaults[build_date]}' images: + # BEGIN TODO REMOVE - matrix: - default: ['4.07.1-flambda'] + default: ['latest'] + base: ['latest'] + coq: ['dev'] + build: + keywords: + - 'dev' + context: './coq' + dockerfile: './dual/dev/Dockerfile' + commit_api: + fetcher: 'github' + repo: 'coq/coq' + branch: 'master' + args: + BASE_TAG: '{matrix[base]}' + COQ_VERSION: '{matrix[coq]}' + COQ_COMMIT: '{defaults[commit]}' + VCS_REF: '{defaults[commit][0:7]}' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' + tags: + # default tag (dev) + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[default]}' + # full tag + - tag: '{matrix[coq]}-ocaml-{matrix[base]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) + - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*-*]}-flambda' + if: '{matrix[base]} != 4.05.0' + # END TODO REMOVE + - matrix: + default: ['latest'] + # default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] coq: ['dev'] build: @@ -73,8 +107,50 @@ images: # # abbreviated tag (*-ocaml-4.07-flambda) # - tag: '{matrix[coq]}-ocaml-{matrix[base][%.*-*]}-flambda' # if: '{matrix[base]} != 4.05.0' + # BEGIN TODO REMOVE + - matrix: + default: ['latest'] + base: ['latest'] + # TODO: Update when appropriate + coq: ['8.13-alpha'] + build: + # TODO: Remove this commit_api section when the beta is released + commit_api: + fetcher: 'github' + repo: 'coq/coq' + branch: 'v8.13' + context: './coq' + # TODO: Replace with "beta/Dockerfile" when the beta is released + dockerfile: './dual/dev/Dockerfile' + keywords: + - '8.13' + args: + BASE_TAG: '{matrix[base]}' + # TODO: Replace with '{matrix[coq]}' when the beta is released + COQ_VERSION: '{matrix[coq][%-*]}.dev' + COQ_COMMIT: '{defaults[commit]}' + # TODO: Replace with 'V{matrix[coq][//-/+]}' when the beta is released + VCS_REF: '{defaults[commit][0:7]}' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' + tags: + # default tag (8.13-alpha) + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[default]}' + # abbreviated tag (8.13) + - tag: '{matrix[coq][%-*]}' + if: '{matrix[base]} == {matrix[default]}' + # full tag + - tag: '{matrix[coq]}-ocaml-{matrix[base]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) + - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*-*]}-flambda' + if: '{matrix[base]} != 4.05.0' + # END TODO REMOVE - matrix: - default: ['4.07.1-flambda'] + default: ['latest'] + # default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] # TODO: Update when appropriate coq: ['8.13-alpha'] @@ -112,8 +188,54 @@ images: # abbreviated tag (*-ocaml-4.07-flambda) - tag: '{matrix[coq][%-*]}-ocaml-{matrix[base][%.*-*]}-flambda' if: '{matrix[base]} != 4.05.0' + # BEGIN TODO REMOVE - matrix: - default: ['4.07.1-flambda'] + default: ['latest'] + base: ['latest'] + coq: ['8.12.1', '8.11.2'] + coq_latest: ['8.12.1'] + build: + context: './coq' + dockerfile: './dual/stable/Dockerfile' + args: + BASE_TAG: '{matrix[base]}' + COQ_VERSION: '{matrix[coq]}' + VCS_REF: 'V{matrix[coq]}' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' + tags: + # latest tag + - tag: 'latest' + if: + - '{matrix[coq]} == {matrix[coq_latest]}' + - '{matrix[base]} == {matrix[default]}' + # default tag (8.12.1) + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[default]}' + # abbreviated tag (8.12) + - tag: '{matrix[coq][%.*]}' + if: '{matrix[base]} == {matrix[default]}' + # latest-abbreviated tag (*-ocaml-4.05) + - tag: 'latest-ocaml-{matrix[base][%.*]}' + if: + - '{matrix[coq]} == {matrix[coq_latest]}' + - '{matrix[base]} == 4.05.0' + # latest-abbreviated tag (*-ocaml-4.07-flambda) + - tag: 'latest-ocaml-{matrix[base][%.*-*]}-flambda' + if: + - '{matrix[coq]} == {matrix[coq_latest]}' + - '{matrix[base]} != 4.05.0' + # full tag + - tag: '{matrix[coq]}-ocaml-{matrix[base]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda' + if: '{matrix[base]} != 4.05.0' + # END TODO REMOVE + - matrix: + default: ['latest'] + # default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.10.1-flambda', '4.11.1-flambda'] coq: ['8.12.1', '8.11.2'] coq_latest: ['8.12.1'] @@ -155,8 +277,38 @@ images: # abbreviated tag (*-ocaml-4.07-flambda) - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda' if: '{matrix[base]} != 4.05.0' + # BEGIN TODO REMOVE + - matrix: + default: ['latest'] + base: ['latest'] + coq: ['8.10.2', '8.9.1', '8.8.2', '8.7.2'] + build: + context: './coq' + dockerfile: './dual/stable/Dockerfile' + args: + BASE_TAG: '{matrix[base]}' + COQ_VERSION: '{matrix[coq]}' + VCS_REF: 'V{matrix[coq]}' + COQ_EXTRA_OPAM: 'coq-native coq-bignums' + tags: + # default tag (8.10.2) + - tag: '{matrix[coq]}' + if: '{matrix[base]} == {matrix[default]}' + # abbreviated tag (8.10) + - tag: '{matrix[coq][%.*]}' + if: '{matrix[base]} == {matrix[default]}' + # full tag + - tag: '{matrix[coq]}-ocaml-{matrix[base]}' + # abbreviated tag (*-ocaml-4.05) + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*]}' + if: '{matrix[base]} == 4.05.0' + # abbreviated tag (*-ocaml-4.07-flambda) + - tag: '{matrix[coq][%.*]}-ocaml-{matrix[base][%.*-*]}-flambda' + if: '{matrix[base]} != 4.05.0' + # END TODO REMOVE - matrix: - default: ['4.07.1-flambda'] + default: ['latest'] + # default: ['4.07.1-flambda'] base: ['4.05.0', '4.07.1-flambda', '4.08.1-flambda', '4.09.1-flambda'] coq: ['8.10.2', '8.9.1', '8.8.2', '8.7.2'] build: