A few days ago I told someone that Coq is getting renamed into Rocq. They are not active in the community so they hadn’t heard. They were surprised and a bit skeptical at first, so they searched for the project homepage coq.inria.fr and they noticed that… there is no mention of the new name whatsoever.
I was physically in a room where @mattam82 announced the rename, so I know that it has been officially decided. But it’s still pretty bizarre that, after many months, there is no visible change to the webpage.
Am I missing something, are there clear mentions of Rocq somewhere in the official Coq spaces? If I want to “prove” to someone that a rename has been decided, what sort of evidence is the easiest to find?
I understand that changing all Coq resources around is an enormous amount of work, that will not happen overnight and never be fully finished. But adding a mention of the new name on the official landing page seems like an obvious first step.
Regarding proof, it is found on the not-so-easy-to-find roadmap.
For the rest I cannot tell you.
Some more information from @Zimmi48 on the github PR:
That’s not the official position of the Coq team, which is instead that as long as the renaming hasn’t happened, people should still refer to Coq as Coq: x.com
My understanding is that the plan that the Coq team has in mind is not of a gradual transition, starting when the rename was announced (this is what I naively assumed), but rather of a big-bang rename event that will come someday in the future, before which the name has not actually changed.
(As far as I can tell there is no publicly available information about the current state of the renaming work; @herbelin mentioned on the PR that the current plan is to have the transition happen sometime in 2024.)
In other words, I misunderstood: The Coq team has not decided to rename Coq into Rocq, but that they have decided that they will rename Coq into Rocq, someday in the future.
The nonexistent communication about this is no big deal, it’s as expected for a project largely managed by volunteers juggling with other obligations; but I think that it’s unfortunate for a topic (the name change) that was widely discussed and in which the whole community got actively involved.
The topic is now “solved”, in that there is a clearly-visible sign of the upcoming Coq->Rocq rename on the coq website. Thanks to everyone who participated, and in particular to @Zimmi48 who suggested the wording that ended up on the webpage.