Karl Palmskog (Aug 18 2020 at 19:43): Karl Palmskog (Aug 18 2020 at 19:43):Rudi Grinberg said:
The way we gained quick adoption of dune in OCaml is by keeping maximum compatibility with all the dune metadata written by users. I don't think it would be very hard to keep things compatible for coq projects either.
Well, if you and Emilio could come out with a Dune Coq language version (say, 0.3) and say that this version will not refuse to build with Dune going forward, I would be less reluctant. Note that many Coq project releases still contain dune/dune-project, it's just that we don't use those for the official builds.
To be precise, what I don't want to happen is that a user installs Dune 3.5 in the year 2023 and finds out that no Coq projects compatible with Coq 8.13 can be built by Dune 3.5. Due to the research entrenchment of Coq, many are using very old Coq versions for research.
Rudi Grinberg (Aug 18 2020 at 19:46):Yeah let's see what Emilio has to say. Usually, it's not very hard to maintain compatibility for old rules. But it depends on the changes Emilio has in mind.
Karl Palmskog (Aug 18 2020 at 19:48):@Rudi Grinberg maybe I should open an issue about this in the Dune repo, or what do you think?
Rudi Grinberg (Aug 18 2020 at 19:48):To be precise, what I don't want to happen is that a user installs Dune 3.5 in the year 2023 and finds out that no Coq projects compatible with Coq 8.13 can be built by Dune 3.5. Due to the research entrenchment of Coq, many are using very old Coq versions for research.
If a user can build an old version of Coq, then building an old version of dune is surely not out of reach. However, I do agree that this should be avoided if possible. Compatibility is an incredibly important feature that I'm glad we've capitalized on in dune.
Rudi Grinberg (Aug 18 2020 at 19:51):Karl Palmskog said:
Rudi Grinberg maybe I should open an issue about this in the Dune repo, or what do you think?
Whatever works better for you. I think all interested parties follow dune's issue tracker and this zulip server regardless.
Karl Palmskog (Aug 18 2020 at 19:55):OK, let's just ping @Emilio Jesús Gallego Arias and see if he would find a summary of the above helpful or simply reading this Zulip topic is enough (potential GitHub issue topic would be: "Guarantees about backwards compatibility of Coq builds before language version 1.0")
Karl Palmskog (Aug 31 2020 at 18:59):@Emilio Jesús Gallego Arias could you comment on current plans for using coq 0.x? It would be really nice to see more projects using Dune in the Coq opam archive, but on the other hand, we don't want to make them unbuildable a year from now.
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:07):@Karl Palmskog all that I can say for now is that 0.x versions won't indeed have long-term support
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:07):I'm working towards 1.0 version
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:07):as soon as possible
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:10):It is very likely that the semantics of (coq.theories ) does indeed change
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:10):so until we settle that out I'm a bit wary of commiting to long-term support
Karl Palmskog (Aug 31 2020 at 19:16):OK, so basically it's going to be an "all-or-nothing" using coq 1.0 for stability. Well, at least we can plan accordingly, e.g., most of my projects currently have "fallback" coq_makefile support.
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:18):We will keep support for 0.x versions for as long as we can
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:18):tho
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:18):it is not like they will be removed
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:19):but once 1.0 comes alive, they will emit a warning
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:19):1.0 shouldn't take long tho
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:19):I have scheduled significant cycles to try to close it ASAP
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:21):By the way @Karl Palmskog , where is the issue for multiple binding of logical paths?
Karl Palmskog (Aug 31 2020 at 19:22):Emilio Jesús Gallego Arias said:
it is not like they will be removed
But you said the following in the coq-community issue:
Moreover, when we reach 1.0 , we will likely deprecate all other lang versions, and give like 3/5? releases for people to adapt.
To me, the "3/5? releases" would mean it will be removed eventually.
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:22):Yup at some point
Emilio Jesús Gallego Arias (Aug 31 2020 at 19:23):I prefer to give a very low bound :)
Last updated: Jun 04 2023 at 23:30 UTC