Stream: Dune devs & users

Topic: Backwards compatibility for building Coq projects with Dune


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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")

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:07):

I'm working towards 1.0 version

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:07):

as soon as possible

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:10):

It is very likely that the semantics of (coq.theories ) does indeed change

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:18):

tho

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:18):

it is not like they will be removed

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:19):

but once 1.0 comes alive, they will emit a warning

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:19):

1.0 shouldn't take long tho

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:19):

I have scheduled significant cycles to try to close it ASAP

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:22):

Yup at some point

view this post on Zulip Emilio Jesús Gallego Arias (Aug 31 2020 at 19:23):

I prefer to give a very low bound :)


Last updated: Oct 16 2021 at 09:07 UTC