Upgrade to Dune ≥ 3.8.2 (namely: 3.9.1)

[palmskog]

Dune 3.8.2 is now out on opam and it fixes a serious Coq-related bug (ocaml/dune#7893) that made it difficult to use Dune-Coq 0.8 in projects that depend on plugins. Any chance of upgrading the usual Coq Docker images to use this version of Dune?

As one (successful) test, I tried out Dune 3.8.2 by unpinning Dune in one of the projects I help maintain: runtimeverification/vlsm#239

[erikmd]

@himito could you please take care of addressing:

• this issue Upgrade to Dune ≥ 3.8.2 (namely: 3.9.1) #57 by upgrading docker-base/images.yml to bump dune's version (maybe to 3.8.2, maybe to the latest if no regression is known)
• this Zulip comment by upgrading docker-coq/images.yml to distribute coqorg/coq:8.17.1

— sorry but I'm extremely busy with grading since last week, with a pending deadline at the end of this week…

[himito]

Hi @erikmd,

OK, I will try to do this today.

Cheers,
Jaime

[Alizter]

FTR we are already on 3.9 for Dune. Importantly in 3.8.3 there were some Windows specific fixes. I would recommend 3.9. There will be no difference for Coq from 3.8.2 onwards however.

[erikmd]

Thanks!

FYI @himito the build failed:
https://gitlab.com/coq-community/docker-base/-/pipelines/923577368
because even if dune 3.9.1 was released in https://github.com/ocaml/dune/releases,
it is not yet available as an opam package: https://opam.ocaml.org/packages/dune/
there should be a PR open in https://github.com/ocaml/opam-repository,
so, let's monitor https://opam.ocaml.org/packages/dune/ and we'll restart the build afterwards

[Alizter]

3.9.1 was released shortly after I wrote the above, so a PR ought to come today.

[palmskog]

After an opam-repository PR of Dune appears, it usually takes something like 40-50 hours before it is actually merged and appears via opam update. Please consider using 3.9.0 instead.

[Alizter]

• [new release] dune (15 packages) (3.9.1) ocaml/opam-repository#24073

[Alizter]

@palmskog took < 24 hours this time.

[palmskog]

There's still something like 10h left after the merge before it appears via opam update.

[erikmd]

FYI, all the necessary steps have now been completed by @himito and me, so
all docker-coq & docker-mathcomp images are now up-to-date with dune.3.9.1:

• https://explore.ggcr.dev/?repo=coqorg/base
• https://explore.ggcr.dev/?repo=coqorg/coq
• https://explore.ggcr.dev/?repo=mathcomp/mathcomp

e.g. https://explore.ggcr.dev/?image=mathcomp/mathcomp:latest-coq-8.16
yields "DUNE_VERSION=3.9.1", cf. https://explore.ggcr.dev/?blob=mathcomp/mathcomp@sha256:2b58513081e9825fe0a1e86c1fe1da1c2dc198e3bbbc9f776636b632b3aae4ed&mt=application%2Fvnd.docker.container.image.v1%2Bjson&size=12597&manifest=mathcomp/mathcomp:latest-coq-8.16@sha256:8d2d3949ac9145686de35a8c717dc818435fe211b95d94c42c63c428ee84e0e9

Meanwhile, coqorg/coq:8.17 now ships coq.8.17.1.

i.e. https://explore.ggcr.dev/?image=coqorg/coq:8.17
yields "COQ_VERSION=8.17.1", cf. https://explore.ggcr.dev/?blob=coqorg/coq@sha256:51115ed672ae6c0dd21dc82832077e626eeedf9779fc1beb42d326de691f0252&mt=application%2Fvnd.docker.container.image.v1%2Bjson&size=10813&manifest=coqorg/coq:8.17@sha256:e419463f35c91298b8eb1b565c2869d3fd2d13c26eb203c192e1a65dddbb8fa5

Sorry for announcing this a bit late than you might expect; it happens the last upgrade/rebuild in docker-mathcomp was hindered by docker-hub network issues in gitlab.inria.fr…
anyway I filed an issue in coqbot, so @Zimmi48 and I can try to better mitigate this issue in the future.

Really: What would we do without coqbot? It does help much 👍