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 2 commits
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
7 changes: 7 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,13 @@
<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 use both names, for example
by writing "formalized with Rocq (formerly Coq)" or "formalized with Coq (also named Rocq)".
Copy link
Member

Choose a reason for hiding this comment

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

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

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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

</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 Proof Assistant, the Rocq prover</title>
<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