Stream: Coq Platform devs & users

Topic: Dune version requirements in 2021.09


view this post on Zulip Karl Palmskog (Sep 11 2021 at 10:41):

Since 8.14.0 will require Dune, should the platform maybe mandate/set a certain version of Dune? As can be seen here, the Dune version can have a lot of consequences. Also some discussion in my old issue.

In an ideal future, the Dune Coq maintainers (Emilio and Rudi) could give a figurative stamp of approval to some Dune version for a platform release.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2021 at 10:55):

I think we require Dune >= 2.5.0 for 8.14, that's all. Other users of course may have different requirements.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2021 at 10:55):

Dune for .v files is still experimental, so the platform deals only with the .ml parts of Coq

view this post on Zulip Karl Palmskog (Sep 11 2021 at 10:56):

sure, 2.5.0 is the minimum necessary version. But if platform users get some Dune >= 2.9, this gives a much better experience, coq-native support, etc., which was my point.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2021 at 11:00):

Ah, sure, for both OCaml and Dune, it makes sense to ship the latest versions

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2021 at 11:00):

and in general for all accessory software

view this post on Zulip Karl Palmskog (Sep 11 2021 at 11:00):

one use case discussed from the beginning is to use the platform for research artifacts ("just get platform 20XX-YY-ZZ and this will work"). If you don't know the Dune version in the platform, you have to support any choice of Dune >= 2.5.0 for an artifact which may combine Coq and OCaml, which is a big pain

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2021 at 11:01):

Sure the version should be specified; now that opam 2.1 supports lockfiles tho, that's easy to actually specify in the repository

view this post on Zulip Michael Soegtrop (Sep 11 2021 at 14:58):

@Karl Palmskog : thanks for pointing this out. Sure I can put a specific dune version in the package versions file. A one liner elaborating why we don't use just what is in the Coq opam package would be nice.

view this post on Zulip Karl Palmskog (Sep 11 2021 at 17:33):

not sure I understand about the one-liner. For example, we could say right now that we consciously choose Dune 2.9.1, which happens to be the latest release as of September 2021, to get the benefits of quality-of-life improvements and bug fixes when building Coq projects (and when building Coq), as well as coq-native compilation support, compared to versions in the range 2.5.0 to 2.8.X.

If the 2021.09 platform then has an upgrade (e.g., 2021.09.0 -> 2021.09.1), then a judgment call is made whether to upgrade Dune or keep 2.9.1 as-is. If no platform-related Dune problems have been reported, then probably stick with 2.9.1.

view this post on Zulip Théo Zimmermann (Sep 12 2021 at 08:18):

@Michael Soegtrop We pin all end-users library to a specific version and document them as such. Dune could be considered an end-user tool in the platform and therefore pinned in the same way.

view this post on Zulip Michael Soegtrop (Sep 12 2021 at 17:15):

@Théo Zimmermann : yes, that's the idea.
@Karl Palmskog : if we simply use the latest version, it doesn't require an explanation, but isn't this what anyway happens if dune is not pinned?

view this post on Zulip Michael Soegtrop (Sep 12 2021 at 17:16):

We don't pin other infrastructure packages, so I am not sure what is special about dune if we could just use the latest one.

view this post on Zulip Karl Palmskog (Sep 12 2021 at 17:23):

then why specify a version for OCaml libraries like menhir and gappa? Why not use whatever the "latest" is?

view this post on Zulip Théo Zimmermann (Sep 12 2021 at 20:49):

The important question IMHO is whether Dune is considered "part of the Coq platform" or "only an infrastructure package / dependency".


Last updated: Jan 30 2023 at 11:03 UTC