Stream: coq-community devs & users

Topic: ✔ coq:dev Docker tag currently unavailable

Karl Palmskog (May 16 2022 at 14:31):

Heads up that the coq:dev Docker tag is currently unavailable in coqorg on Docker hub. This may make a lot of CI actions in coq-community fail. A workaround is to use the Docker tag coq:dev-ocaml-4.13.1-flambda

Tej Chajed (May 20 2022 at 11:51):

Do you have an estimate for when this will be fixed?

Karl Palmskog (May 20 2022 at 11:54):

I don't personally have an estimate, we will have to check with @Erik Martin-Dorel

Karl Palmskog (May 20 2022 at 11:54):

(I know he is busy with other duties these days)

Théo Zimmermann (May 20 2022 at 12:15):

Yeah, unfortunately this is the exam grading period. I would have offered to help if I wasn't very busy myself with similar tasks.

Tej Chajed (May 20 2022 at 14:15):

No rush, I was just curious.

Erik Martin-Dorel (May 20 2022 at 22:04):

Indeed, sorry @Tej Chajed… I'm swamped with several grading deadlines for the upcoming days… so I can't give a precise ETA, but will definitely try to make some progress in the repo soon!

Just to recall, coqorg/coq:dev had to be removed because of end-of-support for ocaml {4.05, 4.07+1} by coq.master, but currently the following images are still available and continuously updated:

• coqorg/coq:dev-ocaml-4.13-flambda
• coqorg/coq:dev-ocaml-4.12-flambda

Karl Palmskog (May 23 2022 at 13:51):

the above workaround also holds for the mathcomp/mathcomp-dev image (but with lost time due to compiling mathcomp packages)

Matthieu Sozeau (Jun 14 2022 at 09:38):

It seems that the issue also affects the 8.14 versions, e.g. coqorg/coq:8.14-ocaml-4.12-flambda is no longer found, is that expected?
(it breaks the metacoq CI on our 8.14 branch)

Pierre Roux (Jun 14 2022 at 09:41):

According to https://hub.docker.com/r/coqorg/coq/tags?page=1&name=8.14 you can choose ocaml-4.13-flambda and 4.14 but no longer 4.12

Karl Palmskog (Jun 14 2022 at 09:42):

I think 4.12 is skipped because it's no longer among "two latest Ocamls that work with Coq"

Théo Zimmermann (Jun 14 2022 at 09:46):

Indeed. If you don't care about the exact OCaml version and want more stability, coq:8.14 should work fine.

Matthieu Sozeau (Jun 14 2022 at 09:50):

Ok

Erik Martin-Dorel (Jun 14 2022 at 20:26):

@Karl Palmskog, can you mark this Zulip stream as :check: ? apparently only the OriginalPoster can do it.

(FTR, the corresponding GitHub issue, now closed, was coq-community/docker-coq#46)

Notification Bot (Jun 14 2022 at 20:58):

Ali Caglayan has marked this topic as resolved.

Last updated: Jun 03 2023 at 17:29 UTC