Karl Palmskog (Sep 11 2021 at 10:41): 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.
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.
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
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.
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
Emilio Jesús Gallego Arias (Sep 11 2021 at 11:00):and in general for all accessory software
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
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
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.
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.
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.
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?
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.
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?
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: Jun 03 2023 at 05:01 UTC