From e4fb1d3cbbceaabb6898bc12576cbdae58c0eea1 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 30 Apr 2025 15:46:50 +0200 Subject: [PATCH 1/3] fix: s/9.00/9.0/ --- images.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/images.yml b/images.yml index 1142af3..dd44c28 100644 --- a/images.yml +++ b/images.yml @@ -25,7 +25,7 @@ images: # # - tag: 'latest-coq-{matrix[coq]}' - matrix: - coq: ['dev', '9.00', '8.20', '8.19'] + coq: ['dev', '9.0', '8.20', '8.19'] mathcomp: ['2.4.0'] build: # keyword for docker-keeper's trigger (from docker-coq CI) From 5e8783a112f44509ab333e7697b79fd1af62b90a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 30 Apr 2025 16:31:25 +0200 Subject: [PATCH 2/3] feat: Fix input Docker image and output Docker tag for rocq-prover MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With this patch: - the tag latest-coq-8.20 is built from coqorg/coq:8.20-ocaml-4.14 - the tag latest-rocq-prover-9.0 … from rocq/rocq-prover:9.0-ocaml-4.14 --- images.yml | 52 +++++++++++++++++++++++++++----------- mathcomp/single/Dockerfile | 2 +- 2 files changed, 38 insertions(+), 16 deletions(-) diff --git a/images.yml b/images.yml index dd44c28..029bcb6 100644 --- a/images.yml +++ b/images.yml @@ -4,39 +4,61 @@ active: true gitlab_ci_tags: - 'large' args: - COQ_TAG: '{matrix[coq]}-ocaml-4.14-flambda' + COQ_TAG: 'coqorg/coq:{matrix[coq]}-ocaml-4.14-flambda' MATHCOMP_VERSION: '{matrix[mathcomp]}' docker_repo: 'mathcomp/mathcomp' images: # TODO: Copy and Uncomment at next mathcomp (beta or stable) release # - matrix: - # coq: ['dev', '8.16', '8.15', '8.14', '8.13'] + # rocq: ['dev', '8.16', '8.15', '8.14', '8.13'] # mathcomp: ['1.16+beta1'] # build: - # # keyword for docker-keeper's trigger (from docker-coq CI) + # # keyword for docker-keeper's trigger (from docker-rocq CI) # keywords: - # - '{matrix[coq]}' + # - '{matrix[rocq]}' # context: './mathcomp' # dockerfile: './single/Dockerfile' + # args: + # # Use docker-keeper/bash_formatter.py syntax to achieve the following: + # # If matrix[rocq] matches "8.*", prepend the version with "coqorg/coq:", + # # otherwise, prepend the version with "rocq/rocq-prover:" + # COQ_TAG: '{matrix[rocq][/#/,][//,8.*/coqorg/coq:][//,*/rocq/rocq-prover:]}{matrix[rocq]}-ocaml-4.14-flambda' # tags: - # - tag: '{matrix[mathcomp][//+/-]}-coq-{matrix[coq]}' - # # TODO at release time: Uncomment "latest-coq-*" and Remove "[//+/-]" - # # TODO after next release: Remove "latest-coq-*" - # # - tag: 'latest-coq-{matrix[coq]}' + # - tag: '{matrix[mathcomp][//+/-]}-rocq-prover-{matrix[rocq]}' + # if: '{matrix[rocq][.*]} != 8' + # - tag: '{matrix[mathcomp][//+/-]}-coq-{matrix[rocq]}' + # if: '{matrix[rocq][.*]} == 8' + # # TODO at release time: Remove "[//+/-]" and Uncomment "latest-*" + # # TODO after next release: Remove "latest-*" + # # - tag: 'latest-rocq-prover-{matrix[rocq]}' + # # if: '{matrix[rocq][.*]} != 8' + # # - tag: 'latest-coq-{matrix[rocq]}' + # # if: '{matrix[rocq][.*]} == 8' - matrix: - coq: ['dev', '9.0', '8.20', '8.19'] + rocq: ['dev', '9.0', '8.20', '8.19'] mathcomp: ['2.4.0'] build: - # keyword for docker-keeper's trigger (from docker-coq CI) + # keyword for docker-keeper's trigger (from docker-rocq CI) keywords: - - '{matrix[coq]}' + - '{matrix[rocq]}' context: './mathcomp' dockerfile: './single/Dockerfile' + args: + # Use docker-keeper/bash_formatter.py syntax to achieve the following: + # If matrix[rocq] matches "8.*", prepend the version with "coqorg/coq:", + # otherwise, prepend the version with "rocq/rocq-prover:" + COQ_TAG: '{matrix[rocq][/#/,][//,8.*/coqorg/coq:][//,*/rocq/rocq-prover:]}{matrix[rocq]}-ocaml-4.14-flambda' tags: - - tag: '{matrix[mathcomp][//+/-]}-coq-{matrix[coq]}' - # TODO after next release: Remove "latest-coq-*" - - tag: 'latest-coq-{matrix[coq]}' + - tag: '{matrix[mathcomp]}-rocq-prover-{matrix[rocq]}' + if: '{matrix[rocq][%.*]} != 8' + - tag: '{matrix[mathcomp]}-coq-{matrix[rocq]}' + if: '{matrix[rocq][%.*]} == 8' + # TODO after next release: Remove "latest-*" + - tag: 'latest-rocq-prover-{matrix[rocq]}' + if: '{matrix[rocq][%.*]} != 8' + - tag: 'latest-coq-{matrix[rocq]}' + if: '{matrix[rocq][%.*]} == 8' - matrix: coq: ['dev', '8.20', '8.19', '8.18', '8.17', '8.16'] @@ -75,7 +97,7 @@ images: - tag: '{matrix[mathcomp]}-coq-{matrix[coq]}' - matrix: - coq: ['dev', '8.20', '8.19', '8.18', '8.17', '8.16'] + coq: ['8.20', '8.19', '8.18', '8.17', '8.16'] mathcomp: ['1.19.0'] build: # keyword for docker-keeper's trigger (from docker-coq CI) diff --git a/mathcomp/single/Dockerfile b/mathcomp/single/Dockerfile index 073c62a..820da42 100644 --- a/mathcomp/single/Dockerfile +++ b/mathcomp/single/Dockerfile @@ -1,5 +1,5 @@ ARG COQ_TAG="dev" -FROM coqorg/coq:${COQ_TAG} +FROM ${COQ_TAG} ARG MATHCOMP_VERSION="dev" ENV MATHCOMP_VERSION=${MATHCOMP_VERSION} From 5e05f204fae69863703f21b5e6fd6686c8e3b9a5 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 30 Apr 2025 16:39:09 +0200 Subject: [PATCH 3/3] chore: Silence a warning that is not critical at all ``` mathcomp/single/Dockerfile:2 DL3006 warning: Always tag the version of an image explicitly ``` Later, we could split the Dockerfile into 2 different ones instead if need be. --- mathcomp/single/Dockerfile | 1 + 1 file changed, 1 insertion(+) diff --git a/mathcomp/single/Dockerfile b/mathcomp/single/Dockerfile index 820da42..8098c33 100644 --- a/mathcomp/single/Dockerfile +++ b/mathcomp/single/Dockerfile @@ -1,4 +1,5 @@ ARG COQ_TAG="dev" +# hadolint ignore=DL3006 FROM ${COQ_TAG} ARG MATHCOMP_VERSION="dev"