fix: s/9.00/9.0/ and (input Docker image, output Docker tag) for (coqorg/coq, rocq/rocq-prover)#34
Conversation
|
Note that the automatically-generated README to be uploaded in Docker Hub at each release (cf. wiki) is available in the I propose to look after this upload myself this time. |
|
BTW I can see in the generated README that "rocq-prover" does not appear in the tag for rocq 9.0, so this would be somewhat inconsistent with these tags: https://hub.docker.com/r/mathcomp/mathcomp-dev/tags I'll push another commit to fix this. |
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
|
I pushed a commit to ensure "input/output compatibility", with "coqorg/coq:8.20" & "rocq/rocq-prover:9.0", using docker-keeper's glob-like syntax. I updated the commented example snippet in the images.yml files so the future releases will be much easier, reusing this patch. Now let's wait for the I'll merge if it succeeds. |
``` 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.
erikmd
changed the title
|
@hoheinzollern the build is on-going: |
|
@erikmd thanks for taking over. I did not fully understand the output of the pipeline failing. |
|
Hi @hoheinzollern,
Yes I'm aware of that, see: I can't fix it right now, but I'm taking a look again ASAP! |
Cc @CohenCyril @hoheinzollern @proux01 FYI Follows-up: rocq-community/docker-coq#79 Follows-up: rocq-community/docker-rocq#13 Follows-up: rocq-community/docker-rocq#11 Follows-up: rocq-community/docker-rocq#14 Follows-up: math-comp/docker-mathcomp#33 Follows-up: math-comp/docker-mathcomp#34
2 participants
Spotted in rocq-community/gaia#27