I saw that the next release after 8.20 is planned to be 9.0, and uses the name Rocq in the documentation. I’m wondering if there’s any public or private roadmap for this renaming.
What I’m especially interested in is what the backwards compatibilty guarantee will be. What names will change in version 9, and what will remain for backwards compatibility? It is already challenging to maintain compatibility for two different releases of Coq, and I worry about forcing an atomic upgrade and dropping support for 8.20 all at once if there isn’t code-level compatibility for at least 9.0 and preferably also 9.1.
As one example, the feature to be able to use From Stdlib instead of From Coq isn’t even fully implemented, let alone released.
As documented in Writing Coq libraries and plugins — Coq 8.20.0 documentation we strive to guarantee that it is always possible to get a code that compiles with two successive versions of Coq. This will remain true between Coq 8.20 and Rocq 9. We even plan to provide coq.9.0 compatibility packages with wrapper coq commands for this. For instance, about From Stdlib, the old From Coq keeps working in Rocq 9 (and very likely will for quite a few further versions).
First and foremost, the most important answer to your worry is that the increase in the first version number is not supposed to mean a different compatibility policy compared to a usual major release (which usually only increases the second version number). Coq does not use semantic versioning.
Then, yes, there is a public roadmap specifically for the renaming here: Rocq 9.0 roadmap (essential renaming items) · GitHub
Then, there is work on a long-term roadmap for Rocq here (and some open PRs to improve it). But I guess, that’s not really what you were asking.
Thanks for those links! It’s great to hear there’s a commitment to supporting compatibility for two consecutive versions, and that this will continue. I was not under the impression that Coq was using this as a semantic version “major version bump”, but glad you clarified that.