From 65e25d9553392f5ed5f7091d163d2bbdc0c5e16d Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Thu, 4 Jul 2024 23:06:05 +0200 Subject: [PATCH 1/4] mention the Rocq rename --- incl/footer.html | 6 ++++++ incl/header.html | 4 ++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/incl/footer.html b/incl/footer.html index c304548415..3ede9ae2a7 100644 --- a/incl/footer.html +++ b/incl/footer.html @@ -12,6 +12,12 @@

Recent news

+

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

+
+

There is now a Stack Exchange Q&A site dedicated to Proof Assistants! Do not hesitate to post and answer Coq questions there (use the coq tag).

diff --git a/incl/header.html b/incl/header.html index 1164f150ec..5d641f118f 100644 --- a/incl/header.html +++ b/incl/header.html @@ -3,7 +3,7 @@ - <#TITLE> | The Coq Proof Assistant + <#TITLE> | The Coq/Rocq Proof Assistant @@ -30,7 +30,7 @@ -

The Coq Proof Assistant

+

The Coq/Rocq Proof Assistant

From e3974f32ec8b38102a632ec7b1e002b6713f63b7 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Fri, 5 Jul 2024 09:48:34 +0200 Subject: [PATCH 2/4] new iteration after feedback from silene --- incl/footer.html | 3 ++- incl/header.html | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/incl/footer.html b/incl/footer.html index 3ede9ae2a7..0b3b9e79d1 100644 --- a/incl/footer.html +++ b/incl/footer.html @@ -14,7 +14,8 @@

Recent news

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

diff --git a/incl/header.html b/incl/header.html index 5d641f118f..d60342a823 100644 --- a/incl/header.html +++ b/incl/header.html @@ -3,7 +3,7 @@ - <#TITLE> | The Coq/Rocq Proof Assistant + <#TITLE> | The Coq Proof Assistant, the Rocq prover @@ -30,7 +30,7 @@ -

The Coq/Rocq Proof Assistant

+

The Coq (Rocq) Proof Assistant

From 5b56e1512f3c6c02a912f9687f4601851d51ed2c Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Fri, 5 Jul 2024 11:38:26 +0200 Subject: [PATCH 3/4] new iteration: only a 'news' item --- incl/footer.html | 6 +----- incl/header.html | 4 ++-- 2 files changed, 3 insertions(+), 7 deletions(-) diff --git a/incl/footer.html b/incl/footer.html index 0b3b9e79d1..68d64fd094 100644 --- a/incl/footer.html +++ b/incl/footer.html @@ -12,11 +12,7 @@

Recent news

-

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

+

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.

There is now a Stack Exchange Q&A site dedicated to Proof Assistants! Do not hesitate to post and answer Coq questions there (use the coq tag).

diff --git a/incl/header.html b/incl/header.html index d60342a823..1164f150ec 100644 --- a/incl/header.html +++ b/incl/header.html @@ -3,7 +3,7 @@ - <#TITLE> | The Coq Proof Assistant, the Rocq prover + <#TITLE> | The Coq Proof Assistant @@ -30,7 +30,7 @@ -

The Coq (Rocq) Proof Assistant

+

The Coq Proof Assistant

From 77c29944c48158fae3278aaae79f38e9da820606 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Fri, 5 Jul 2024 15:06:43 +0200 Subject: [PATCH 4/4] new iteration with more context information --- incl/footer.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/incl/footer.html b/incl/footer.html index 68d64fd094..6618302e27 100644 --- a/incl/footer.html +++ b/incl/footer.html @@ -12,7 +12,7 @@

Recent news

-

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.

+

The Coq team has decided that Coq will be renamed into 'The Rocq Prover'. Background information available here. 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.

There is now a Stack Exchange Q&A site dedicated to Proof Assistants! Do not hesitate to post and answer Coq questions there (use the coq tag).