Merge PR rocq-prover#20026: Rename Coq -> Rocq in various comments and doc

Reviewed-by: ppedrot
Ack-by: silene
Co-authored-by: ppedrot <[email protected]>

Author: coqbot-app[bot]

.gitlab-ci.yml

@@ -64,7 +64,7 @@ before_script:
   - dev/tools/list-potential-artifacts.sh > downloaded_artifacts.txt
   - dev/ci/gitlab-section.sh end before_script
 
-# Regular "release" build of Coq, with final installed layout
+# Regular "release" build of Rocq, with final installed layout
 .build-template:
   stage: build-0
   interruptible: true
@@ -141,7 +141,7 @@ before_script:
     name: "$CI_JOB_NAME"
     expire_in: 2 months
 
-# The used Coq must be set explicitly for each job with "needs:".
+# The used Rocq must be set explicitly for each job with "needs:".
 # We add a spurious dependency `not-a-real-job` that must be
 # overridden otherwise the CI will fail (to help debugging missing needs).
 
@@ -607,7 +607,7 @@ validate:edge+flambda:
     OPAM_VARIANT: "+flambda"
   only: *full-ci
 
-# Libraries are by convention the projects that depend on Coq
+# Libraries are by convention the projects that depend on Rocq
 # but not on its ML API
 
 library:ci-argosy:
@@ -1054,7 +1054,7 @@ library:ci-trakt:
   - plugin:ci-elpi_hb
   stage: build-2
 
-# Plugins are by definition the projects that depend on Coq's ML API
+# Plugins are by definition the projects that depend on Rocq's ML API
 
 plugin:ci-aac_tactics:
   extends: .ci-template-flambda

.mailmap

@@ -1,4 +1,4 @@
-## Coq contributors
+## Rocq contributors
 ##
 ## This file allows joining the different accounts of a same person.
 ## Cf for instance: git shortlog -nse. More details via: man git shortlog

CODE_OF_CONDUCT.md

@@ -1,6 +1,6 @@
-# Coq Code of Conduct #
+# Rocq Code of Conduct #
 
-The Coq development team and the user community are made up of a mixture of
+The Rocq development team and the user community are made up of a mixture of
 professionals and volunteers from all over the world.
 Diversity brings variety of perspectives that can be very valuable, but it can
 also lead to communication issues and unhappiness. Therefore, we have a few
@@ -9,12 +9,12 @@ participation in our community a positive experience for
 everyone.
 These rules apply equally to core developers (who should lead by example),
 occasional contributors and those seeking help and guidance.
-Their goal is that everyone feels safe and welcome when contributing to Coq or
-interacting with others in Coq related forums.
+Their goal is that everyone feels safe and welcome when contributing to Rocq or
+interacting with others in Rocq related forums.
 
-These rules apply to all spaces managed by the Coq development team.
+These rules apply to all spaces managed by the Rocq development team.
 This includes the GitHub repository, the Discourse forum, the Zulip chat, the mailing lists,
-physical events like Coq working groups and workshops, and any other forums
+physical events like Rocq working groups and workshops, and any other forums
 created or managed by the development team which the community uses for
 communication. In addition, violations of these rules outside these spaces may
 affect a person's ability to participate within them.
@@ -34,7 +34,7 @@ affect a person's ability to participate within them.
   behavior and poor manners. We might all experience some frustration now and
   then, but we cannot allow that frustration to turn into a personal attack.
   It's important to remember that a community where people feel uncomfortable
-  or threatened is not a productive one. Members of the Coq development team
+  or threatened is not a productive one. Members of the Rocq development team
   and user community should be respectful when dealing with other members as
   well as with people outside the community.
 - **Be careful in the words that you choose.**
@@ -55,11 +55,11 @@ affect a person's ability to participate within them.
   Consider what image your words will give to outsiders of the development
   team / the user community as a whole. Try to avoid references to private
   knowledge to be understandable by anyone.
-- **Coq online forums are only to discuss Coq-related subjects.**
+- **Rocq online forums are only to discuss Rocq-related subjects.**
   Unrelated political discussions or long digressions are unwelcome,
   even for illustration or comparison purposes.
 - **When we disagree, try to understand why.**
-  Disagreements, both social and technical, happen all the time and Coq is no
+  Disagreements, both social and technical, happen all the time and Rocq is no
   exception. It is important that we resolve disagreements and differing views
   constructively. Remember that we are different. Different people
   have different perspectives on issues. Being unable to understand why someone
@@ -93,13 +93,13 @@ affect a person's ability to participate within them.
   harmless individually but, over time, contribute to a hostile
   environment.
 
-## Interaction on Coq forums (Zulip, Discourse, etc.) ##
+## Interaction on Rocq forums (Zulip, Discourse, etc.) ##
 
 Anyone is welcome to ask questions and bring answers, provided they
 respect the aforementioned rules. In addition we ask that
 - you do your best to put your questions into their context by
-  providing Coq code or pointers to it, and enough indications to
-  understand where the Coq goals or error message come from.
+  providing Rocq code or pointers to it, and enough indications to
+  understand where the Rocq goals or error message come from.
 - if you are running through educational material, we kindly ask you
   to explicitly state it, and that answers do not solve such exercises
   for you, but only provide hints.
@@ -119,7 +119,7 @@ what answers they are likely to receive.
 ## Enforcement ##
 
 If you believe someone is violating the code of conduct, we ask that you report
-it by emailing the Coq Code of Conduct enforcement team at
+it by emailing the Rocq Code of Conduct enforcement team at
 <[email protected]> or, at your discretion, any member of the team.
 Confidentiality with regard to the reporter of an
 incident will be maintained while dealing with it.
@@ -135,9 +135,9 @@ communications brought to their attention.
 
 Depending on the violation, the team can choose to address a private or public
 warning to the offender, request an apology, or ban them for a short or a long
-period from interacting on one or all spaces managed by the Coq
+period from interacting on one or all spaces managed by the Rocq
 development team (both online and offline).
-The ban may apply to anyone, including members of the Coq development
+The ban may apply to anyone, including members of the Rocq development
 team, in which case the developer will lose their privileges for the
 duration of the ban and may need to rebuild trust to regain them.
 

Makefile

@@ -8,7 +8,7 @@
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
 
-# Dune Makefile for Coq
+# Dune Makefile for Rocq
 
 .PHONY: help help-install states world coqide watch check    # Main developer targets
 .PHONY: refman-html refman-pdf corelib-html apidoc     # Documentation targets
@@ -35,15 +35,15 @@ HIDE := $(if $(VERBOSE),,@)
 
 help:
 	@echo ""
-	@echo "Welcome to Coq's Dune-based build system. If you are final user type"
+	@echo "Welcome to Rocq's Dune-based build system. If you are final user type"
 	@echo "make help-install for installation instructions. Common developer targets are:"
 	@echo ""
-	@echo "  - states: build a minimal functional coqtop"
+	@echo "  - states: build a minimal functional rocq repl"
 	@echo "  - world:  build main public binaries and libraries in developer mode (no coqide)"
 	@echo "  - watch:  build main public binaries and libraries [continuous build]"
 	@echo "  - coqide: build coqide binary in developer mode"
 	@echo "  - check:  build all ML files as fast as possible"
-	@echo "  - test-suite: run Coq's test suite [env NJOBS=N to set job parallelism]"
+	@echo "  - test-suite: run Rocq's test suite [env NJOBS=N to set job parallelism]"
 	@echo "  - dunestrap: Generate the dune rules for vo files"
 	@echo ""
 	@echo "  Note: running ./configure is not recommended for developers,"
@@ -58,9 +58,9 @@ help:
 	@echo ""
 	@echo " Documentation targets:"
 	@echo ""
-	@echo "  - refman-html: build Coq's reference manual [HTML version]"
-	@echo "  - refman-pdf:  build Coq's reference manual [PDF version]"
-	@echo "  - corelib-html: build Coq's Corelib documentation [HTML version]"
+	@echo "  - refman-html: build Rocq's reference manual [HTML version]"
+	@echo "  - refman-pdf:  build Rocq's reference manual [PDF version]"
+	@echo "  - corelib-html: build Rocq's Corelib documentation [HTML version]"
 	@echo "  - apidoc:      build ML API documentation"
 	@echo ""
 	@echo " Miscellaneous targets:"
@@ -77,7 +77,7 @@ help:
 
 dev-targets:
 	@echo ""
-	@echo "In order to get a functional Coq install layout, the world target is required."
+	@echo "In order to get a functional Rocq install layout, the world target is required."
 	@echo "However, This is often inconvenient for developers, due to the large amount of"
 	@echo "files that world will build. We provide some useful subtargets here:"
 	@echo ""
@@ -86,8 +86,8 @@ dev-targets:
 
 help-install:
 	@echo ""
-	@echo "The Dune-based Coq build is split into several packages; see Dune and dev/doc"
-	@echo "documentation for more details. A quick install of Coq alone can be done with"
+	@echo "The Dune-based Rocq build is split into several packages; see Dune and dev/doc"
+	@echo "documentation for more details. A quick install of Rocq alone can be done with"
 	@echo ""
 	@echo " $$ ./configure -prefix <install_prefix>"
 	@echo " $$ make dunestrap"
@@ -98,12 +98,12 @@ help-install:
 	@echo ""
 	@echo "  - rocq-runtime: base Rocq package, toplevel compilers, plugins, tools, no corelib, no stdlib, no GTK"
 	@echo "  - coq-core: compat binaries (coqc instead of rocq compile, etc)"
-	@echo "  - rocq-core: Coq's prelude and corelib"
+	@echo "  - rocq-core: Rocq's prelude and corelib"
 	@echo "  - coqide-server: XML protocol language server"
 	@echo "  - coqide: CoqIDE gtk application"
 	@echo "  - rocq: meta package depending on rocq-runtime rocq-core rocq-stdlib"
 	@echo "    (also calls the test suite when using --with-test)"
-	@echo "  - coq: meta package depending on rocq-runtime coq-core rocq-core rocq-stdlib coq-stdlib"
+	@echo "  - coq: meta package depending on rocq coq-core coq-stdlib"
 	@echo "    (also calls the test suite when using --with-test)"
 	@echo ""
 	@echo " To build a package, you can use:"
@@ -116,7 +116,7 @@ help-install:
 	@echo "  - 'dune install --prefix=<install_prefix> package'"
 	@echo ""
 	@echo " Note that '--prefix' must be passed to dune install. The '-prefix' passed to"
-	@echo " configure tells Coq where to look for libraries."
+	@echo " configure tells Rocq where to look for libraries."
 	@echo ""
 	@echo " Note that building a package in release mode ignores other packages present in"
 	@echo " the worktree. See Dune documentation for more information."
@@ -197,7 +197,7 @@ release: theories/dune
 
 # We define this target as to override Make's built-in one
 install:
-	@echo "To install Coq using dune, use 'dune build -p P && dune install P'"
+	@echo "To install Rocq using dune, use 'dune build -p P && dune install P'"
 	@echo "where P is any of the packages defined by opam files in the root dir"
 	@false
 
@@ -252,9 +252,9 @@ export CI_PURE_DUNE
 include Makefile.ci
 
 # Custom targets to create subsets of the world target but with less
-# compiled files. This is desired when we want to have our Coq Dune
-# build with Coq developments that are not dunerized and thus still
-# expect an install layout with a working Coq setup, but smaller than
+# compiled files. This is desired when we want to have our Rocq Dune
+# build with Rocq developments that are not dunerized and thus still
+# expect an install layout with a working Rocq setup, but smaller than
 # world.
 #
 # Unfortunately, Dune still lacks the capability to refer to install

boot/dune

@@ -1,9 +1,9 @@
 ; This library must have no dependencies except config, as it is a
-; dependency for most Coq command line tools.
+; dependency for most Rocq command line tools.
 (library
  (name boot)
  (public_name rocq-runtime.boot)
- (synopsis "Coq Enviroment and Paths facilities")
+ (synopsis "Rocq Enviroment and Paths facilities")
  ; until ocaml/dune#4892 fixed
  ; (private_modules util)
  (libraries rocq-runtime.config))

boot/env.mli

@@ -8,9 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Coq runtime enviroment API.
+(** Rocq runtime enviroment API.
 
-This module provides functions for manipulation of Coq's runtime
+This module provides functions for manipulation of Rocq's runtime
 enviroment, including the standard directories and support files.
 
 This API is similar in spirit to findlib's or dune-sites API,
@@ -21,7 +21,7 @@ see their documentation for more information:
 
 It is important that this library has a minimal dependency set.
 
-The Coq runtime enviroment needs to be properly initialized before use;
+The Rocq runtime enviroment needs to be properly initialized before use;
 we detail the rules below. It is recommended that applications requiring
 multiple accesses to the environment, do initialize it once and keep a ref
 to it. We don't forbid yet double initialization, (second time is a noop)
@@ -44,7 +44,7 @@ as of now this sets both [coqlib] and [coqcorelib]; this part of the initializat
 will be eventually moved here.
 
 The error handling policy of this module is simple for now: failing to
-initialize Coq's env will produce a fatal error, and the application will exit with
+initialize Rocq's env will produce a fatal error, and the application will exit with
 code 1. No error handling is thus required on the client yet.
 
 *)
@@ -72,10 +72,10 @@ module Path : sig
 
 end
 
-(** Coq runtime enviroment, including location of Coq's stdlib *)
+(** Rocq runtime enviroment, including location of Rocq's stdlib *)
 type t
 
-(** [init ()] will initialize the Coq environment. *)
+(** [init ()] will initialize the Rocq environment. *)
 val init : unit -> t
 
 (** [stdlib directory] *)

clib/cString.mli

@@ -34,11 +34,11 @@ sig
   (** Remove the eventual first surrounding simple quotes of a string. *)
 
   val quote_coq_string : string -> string
-  (** Quote a string according to Coq conventions (i.e. doubling
+  (** Quote a string according to Rocq conventions (i.e. doubling
       double quotes and surrounding by double quotes) *)
 
   val unquote_coq_string : string -> string option
-  (** Unquote a quoted string according to Coq conventions
+  (** Unquote a quoted string according to Rocq conventions
       (i.e. removing surrounding double quotes and undoubling double
       quotes); returns [None] if not a quoted string *)
 

clib/unicode.mli

@@ -15,7 +15,7 @@ type status
 (** Classify a unicode char into 3 classes or unknown. *)
 val classify : int -> status
 
-(** Return [None] if a given string can be used as a (Coq) identifier.
+(** Return [None] if a given string can be used as a (Rocq) identifier.
     Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *)
 val ident_refutation : string -> (bool * string) option
 

config/coq_config.mli

@@ -34,9 +34,9 @@ val arch : string       (* architecture *)
 (* dubious use in envars, use in coqmakefile *)
 val arch_is_win32 : bool
 
-val version : string    (* version number of Coq *)
-val caml_version : string    (* OCaml version used to compile Coq *)
-val caml_version_nums : int list    (* OCaml version used to compile Coq by components *)
+val version : string    (* version number of Rocq *)
+val caml_version : string    (* OCaml version used to compile Rocq *)
+val caml_version_nums : int list    (* OCaml version used to compile Rocq by components *)
 val vo_version : int32
 
 (* used in envars for coq_makefile *)

config/dune

@@ -1,6 +1,6 @@
 (library
  (name config)
- (synopsis "Coq Configuration Variables")
+ (synopsis "Rocq Configuration Variables")
  (public_name rocq-runtime.config)
  (modules coq_config)
  (wrapped false))
@@ -11,7 +11,7 @@
 
 (library
  (name byte_config)
- (synopsis "Coq Configuration Variables (for bytecode only)")
+ (synopsis "Rocq Configuration Variables (for bytecode only)")
  (public_name rocq-runtime.config.byte)
  (modules coq_byte_config)
  (wrapped false)

coq-core.opam

@@ -2,8 +2,8 @@
 opam-version: "2.0"
 version: "dev"
 synopsis: "Compatibility binaries for Coq after the Rocq renaming"
-maintainer: ["The Coq development team <[email protected]>"]
-authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Rocq development team <[email protected]>"]
+authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"

coq-doc.opam

@@ -9,8 +9,8 @@ algorithms and theorems together with an environment for
 semi-interactive development of machine-checked proofs.
 
 This package provides the Coq Reference Manual."""
-maintainer: ["The Coq development team <[email protected]>"]
-authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Rocq development team <[email protected]>"]
+authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "OPUBL-1.0"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"

coq.opam

@@ -2,8 +2,8 @@
 opam-version: "2.0"
 version: "dev"
 synopsis: "Compatibility metapackage for Coq after the Rocq renaming"
-maintainer: ["The Coq development team <[email protected]>"]
-authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Rocq development team <[email protected]>"]
+authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"

coqide-server.opam

@@ -12,8 +12,8 @@ This package provides the `coqidetop` language server, an
 implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
 which allows clients, such as CoqIDE, to interact with Coq in a
 structured way."""
-maintainer: ["The Coq development team <[email protected]>"]
-authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Rocq development team <[email protected]>"]
+authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"

coqide.opam

@@ -10,8 +10,8 @@ semi-interactive development of machine-checked proofs.
 
 This package provides the CoqIDE, a graphical user interface for the
 development of interactive proofs."""
-maintainer: ["The Coq development team <[email protected]>"]
-authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+maintainer: ["The Rocq development team <[email protected]>"]
+authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
 doc: "https://coq.github.io/doc/"