Please update the version of dune in the docker images to a version that installs .glob files

[JasonGross]

The bug minimizer relies on installed libraries having installed .glob files in order to minimize. Some versions of dune (including 3.13.1) do not install .glob files. Newer versions (3.16.0 and later, according to ocaml/dune#10602 and ocaml/dune@e3f0357) do. Some images (including the 8.19 image) have dune pinned to a version that does not install .glob files. I would appreciate it if all the relatively recent docker images pinned a version of dune that supported .glob files.

See also this Zulip thread

[erikmd]

Belated thanks, @JasonGross and @liyishuai ! (sorry I had missed the notification of your issue, Jason :-/)

Anyway, it turns out that I was reluctant (up to now) to bump dune's version in docker-coq because of this issue:

coq/opam#3090 (comment)

related to this feature of dune:

ocaml/dune#9895

But on second thought, I believe this issue with dune > 3.14 is only related to coq/opam's CI…
which does not rely on docker-coq images directly.

So, we should be on the safe side to bump dune now here I guess…

(and of course, independently of that, we should also fix coq/opam's CI so that it is compatible with a recent dune)

@JasonGross @Zimmi48 @palmskog @himito, does one of you agree with this?

if yes, feel free to comment or react with a 🚀 and I'll merge @liyishuai's PR.

[Zimmi48]

I don't have any concern with bumping the Dune version. I guess @palmskog has more experience with this, but IIRC his concerns with recent Dune versions were more specifically with Coq Dune language versions, not the actual Dune version.

[palmskog]

@Zimmi48 the Dune language version is a concern for Coq projects using Dune and not in Docker CI here.

@erikmd from what I recall, Yves Bertot was able to replicate the problem with Dune locally (likely, dune subst does not support the fact that the home directory contains an opam component). I think the problem will persist in the Coq opam archive CI, but I realize other concerns may be more prioritized.

[erikmd]

OK thanks a lot for your feedback! So let's proceed with this version bump.

The first pipeline is on-going in docker-base (https://gitlab.com/coq-community/docker-base/-/pipelines/1562686654)
which will automatically trigger another one in docker-coq (https://gitlab.com/coq-community/docker-coq/-/pipelines)