Andrew Appel (Apr 21 2022 at 15:19): Andrew Appel (Apr 21 2022 at 15:19):As the developer of a library component of the Coq Platform, I seek opinions from the Coq Platform team about which (older) versions of Coq to support in my tool. The latest release of the Verified Software Toolchain (VST 2.9.1) works under Coq 8.13, Coq 8.14, Coq 8.15. My question is, in the next Coq Platform release, how useful is it to maintain compatibility with Coq 8.13 ? Is there a place where Platform developers can look for guidance about when I can remove 8.13 from my master-branch CI suite? And of course, this question generalizes beyond "Coq Platform 2022.10" to "the next anticipated Platform release" in general.
Karl Palmskog (Apr 21 2022 at 15:25):hmm, we asked in the Coq community survey about how many people were using old versions of Coq, but we asked only about < 8.13 or >= 8.13, and we haven't finished analyzing that part of the survey.
Karl Palmskog (Apr 21 2022 at 15:28):still, if the projected schedule for the next Platform release holds (October 2022 I believe?), Coq 8.13 will be more than 1.5 years old, nearly 2 years old, at that point.
Karl Palmskog (Apr 21 2022 at 15:32):so my view is that supporting the three latest consecutive Coq major versions (8.14 - 8.16) is completely reasonable for a Platform project, and it would be fine to throw out 8.13 right away from CI now that 2022.04 is out
Karl Palmskog (Apr 21 2022 at 15:34):on the other hand, I think there is some consensus that among Platform projects that depend on a library like Stdpp or MathComp, the nice thing to do is to support the same Coq versions as the library does (discussion here)
Karl Palmskog (Apr 21 2022 at 15:41):the closest thing to "guidance" might be Coq's code compatibility policy, which says that it should always be possible for a pure-Coq project to be compatible with two consecutive major versions. In my view, the Platform Team can require or recommend (?) this for pure-Coq projects in the Platform, but no more. Or what do you think, Théo?
Michael Soegtrop (Apr 21 2022 at 16:26):I agree with Karl that supporting 3 major versions of Coq is sufficient.
Please note that Coq Platform supports to install older Coq versions (currently down to 8.12.2) with the latest release, so that e.g. OS compatibility or Coq Platform usability fixes are available for older releases. For example the Coq 8.12.2 in the latest release of Coq Platform is compiled with a different OCaml compiler than the original 8.12.2 release, because the original OCaml version did not work any more on recent Ubuntu releases.
So e.g. for recreation of research artifacts it is not required to support older Coq versions. Instead one can ask people to install an older version of Coq Platform. We try our best to support old releases (ake "picks") of Coq Platform in new releases.
Théo Zimmermann (Apr 21 2022 at 16:29):It's useful to support two consecutive major versions of Coq because new Platform releases generally include an updated pick for the previous version of Coq which tries to be as close as possible from the one for the latest Coq version. But this is it. So supporting three versions or more is not really necessary.
Michael Soegtrop (Apr 21 2022 at 16:32):Let's summarize that supporting two releases is more or less a must have to support smooth transitions. Supporting 3 versions is nice to have and supporting more versions will have little advantage to users.
Last updated: Apr 19 2024 at 12:02 UTC