mention the Rocq rename #241
Conversation
incl/header.html
Outdated
| @@ -3,7 +3,7 @@ | |||
| <html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> | |||
|
|
|||
| <head> | |||
| <title><#TITLE> | The Coq Proof Assistant</title> | |||
| <title><#TITLE> | The Coq/Rocq Proof Assistant</title> | |||
There was a problem hiding this comment.
Keep in mind that Inria has an official trademark on the name Coq (which is recognized in both USA and China, for what that is worth). I have only rudimentary notions on what that implies and it would have to be double-checked with Inria lawyers, but I am pretty sure that such a prominent modification is the fastest way to lose the trademark on Coq.
There was a problem hiding this comment.
My understanding (not a lawyer, etc.):
- Existing versions of Coq released under that name are covered by a Coq trademark and would remain so after a rename of future releases.
- Trademark rights may be lost if the trademark is not used anymore for a period of time (Wikipedia says five years), so (1) any change would only take effect after a few years, when presumably a rename would be deeply in progress and (2) if the website uses a dual naming scheme, Coq and Rocq, then we are still using the trademark and the rights may well be maintained.
Who has asked INRIA lawyers about the rename, and what did they say?
There was a problem hiding this comment.
Writing somewhere on the website that "the Coq proof assistant is also known as the Rocq proof assistant" is presumably fine. Writing "the Coq/Rocq proof assistant" in the title of every single page of the website is no longer a case of dual naming. It is pure single naming.
That said, I have always been a proponent of keeping the Coq prefix in the new name (e.g., Coqatrix) to ease the transition process, but the idea never got enough traction. So, having the tool be renamed Coq/Rocq (Coqroach?) would certainly have my favor. But this ship has long sailed and the plan agreed upon is to get Coq to be renamed into Rocq, not into Coq/Rocq.
As for disclosing on a public forum what was discussed with the lawyers, I would not dare. I suggest you directly phone our coordinator to get a feel of how far the lawyers have progressed on the topic.
There was a problem hiding this comment.
I don't think that people would confuse Coq/Rocq for a single name, but I am happy to try to find a wording that would please you, in that it is clear that Coq and Rocq are both acceptable names for the system.
(Edit: I started ranting a bit about trademarks, but oh well, removed.)
There was a problem hiding this comment.
I just pushed a new version. Instead of using "The Coq/Rocq Proof Assistant", the new version says "The Coq (Rocq) Proof Assistant". Initially I wrote "The Coq Proof Assistant, the Rocq Prover", but this was too large and the banner would overflow on larger zoom level.
The wording in the right menu also does not use Coq/Rocq anymore:
During this transition period, please feel free to use both names, for example by writing "formalized with Rocq (formerly Coq)" or "formalized with Coq (also named Rocq)".
There was a problem hiding this comment.
@tabareau evaluates the arrival time to December. Maybe better to stay on the safe side and be explicit on that, in the style: "planned to be factually renamed the Rocq prover by the end of 2024".
There was a problem hiding this comment.
Here is what I had before (in full):
October 2023: we have decided to rename 'Coq' into 'The Rocq Prover'. Renaming all existing resources is a lot of work, it will be a slow, gradual transition. During this transition period, please feel free to use both names, for example by writing "formalized with Rocq (formerly Coq)" or "formalized with Coq (also named Rocq)".
Would you prefer the following wording, which adds a mention of the 2024 timeline?
October 2023: we have decided to rename 'Coq' into 'The Rocq Prover'. We hope to perform the rename in 2024, but renaming all existing resources is a lot of work so it will be a slow, gradual transition. During this transition period, please feel free to use both names, for example by writing "formalized with Rocq (formerly Coq)" or "formalized with Coq (also named Rocq)".
(Note: I would not recommend any formulation that make it sounds like a complete rename will occur in 2024. This deadline is probably going to be missed, and it's fine, and announcing it too loudly can add pressure to the process.)
incl/footer.html
Outdated
| During this transition period, please feel free to use both names, for example | ||
| by writing "formalized with Rocq (formerly Coq)" or "formalized with Coq (also named Rocq)". |
There was a problem hiding this comment.
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: https://x.com/CoqLang/status/1746558655758041477
That being said, people are free not to respect this (and in practice, some people have already started referring to Coq as Rocq).
In published papers, my personal recommendation would be to add a footnote on the first mention of Coq to say that there is a planned renaming to "the Rocq prover".
There was a problem hiding this comment.
Thanks for the feedback!
I would make this piece of news briefer, though.
Could you suggest a wording that you like, here in the comments?
There was a problem hiding this comment.
@Zimmi48 I made a new iteration that reads as follows (and removes all other changes, as you suggested):
October 2023: we have decided to rename 'Coq' into 'The Rocq Prover'. The rename is currently in preparation, and will hopefully happen sometime in 2024.
incl/footer.html
Outdated
| @@ -12,6 +12,9 @@ | |||
| <div id="block-aggregator-feed-1" class="clear-block block block-aggregator"> | |||
| <h2 class="title">Recent news</h2> | |||
| <div style="background-color: blanchedalmond; padding-left: 5px;" class="content"> | |||
| <p>October 2023: we have decided to rename 'Coq' into 'The Rocq Prover'. The rename is currently in preparation, and will hopefully happen sometime in 2024.</p> | |||
There was a problem hiding this comment.
Here's my suggestion to provide (hopefully) just the right amount of information:
| <p>October 2023: we have decided to rename 'Coq' into 'The Rocq Prover'. The rename is currently in preparation, and will hopefully happen sometime in 2024.</p> | |
| <p>The Coq team has decided that Coq will be renamed into 'The Rocq Prover'. Background information available <a href="https://coq.discourse.group/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001#renaming-coq-8">here</a>. The rename is currently in preparation, we hope to have a new visual identity and website by the end of 2024, and to do a first release of Rocq around that time.</p> |
There was a problem hiding this comment.
Great, thanks! I updated the PR.
There was a problem hiding this comment.
Now the PR looks good to me. I am personally OK to merge this if there is an agreement in @coq/core. This can be obtained by either getting several other core team members approving explicitly this PR and no one rejecting it, or by bringing this to be discussed to the next Coq Call (I won't personally be attending the next Coq Call though, but it could also be the one after).
|
Thanks everyone! |
The Coq team announced a rename months ago, but there is no sign of it on the webpage. This is silly!
The present PR adds just a couple mentions of the new Rocq name, enough for people to know that this is happening for real -- but not enough that it is a lot of work or that tricky questions have to be answered for consistency.
The proposed explanation includes an invitation to use the combined name "Coq/Rocq" during a transition period, so that people that only know of the old name (that is, almost everyone) does not get lost. This is used on the webpage itself, whose title is now "The Coq/Rocq proof assistant."