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.
I think we require Dune >= 2.5.0 for 8.14, that's all. Other users of course may have different requirements.
Dune for .v files is still experimental, so the platform deals only with the .ml parts of Coq
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.
Ah, sure, for both OCaml and Dune, it makes sense to ship the latest versions
and in general for all accessory software
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
Sure the version should be specified; now that opam 2.1 supports lockfiles tho, that's easy to actually specify in the repository
@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.
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.
@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.
@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?
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.
then why specify a version for OCaml libraries like menhir and gappa? Why not use whatever the "latest" is?
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