Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

mention the Rocq rename #241

Merged
merged 4 commits into from
Jul 5, 2024
Merged

mention the Rocq rename #241

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
65e25d9
mention the Rocq rename
gasche Jul 4, 2024
e3974f3
new iteration after feedback from silene
gasche Jul 5, 2024
5b56e15
new iteration: only a 'news' item
gasche Jul 5, 2024
77c2994
new iteration with more context information
Zimmi48 Jul 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions incl/footer.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,12 @@
<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'.
Renaming all existing resources is a lot of work, it will be a slow, gradual transition.
During this transition period, please feel free to mention the proof assistant as Coq/Rocq.
</p>
</div>
<div style="padding-left: 5px;" class="content">
<p>There is now a Stack Exchange Q&amp;A site dedicated to <a href="https://proofassistants.stackexchange.com">Proof Assistants</a>! Do not hesitate to post and answer Coq questions there (use the <a href="https://proofassistants.stackexchange.com/questions/tagged/coq">coq</a> tag).</p>
</div>
<div style="padding-left: 5px;" class="content">
Expand Down
4 changes: 2 additions & 2 deletions incl/header.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@gasche gasche Jul 5, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor Author

@gasche gasche Jul 5, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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)".

Copy link
Member

@herbelin herbelin Jul 5, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@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".

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.)

<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="shortcut icon" href="/files/coq_favicon.ico" type="image/x-icon" />
<link type="text/css" rel="stylesheet" media="all" href="/styles/barron/style.css" />
Expand All @@ -30,7 +30,7 @@
<div id="logo">
<a href="/" title="Home"><img src="/files/barron_logo.png" alt="Home" /></a>
</div>
<h1 class="site-name"><a href="/" title="Home">The Coq Proof Assistant</a></h1>
<h1 class="site-name"><a href="/" title="Home">The Coq/Rocq Proof Assistant</a></h1>
</div><!-- /logo-wrapper-->
</div><!-- /header-->

Expand Down
Loading