From 5c05a916512bdc0dec73cbd5c3f32c91fad657b9 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 11 Jan 2025 12:11:10 +0100 Subject: [PATCH] Rename Coq -> Rocq in INSTALL.md --- INSTALL.md | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index 2beda583df64..be853454e714 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,24 +1,24 @@ Installing From Sources ======================= -To install and use Coq, we recommend relying on [the Coq +To install and use Rocq, we recommend relying on [the Rocq platform](https://github.com/coq/platform/) or on a package manager (e.g. opam or Nix). See https://coq.inria.fr/download and https://github.com/coq/coq/wiki#coq-installation to learn more. -If you need to build Coq from sources manually (e.g. to -contribute to Coq or to write a Coq package), the remainder of this +If you need to build Rocq from sources manually (e.g. to +contribute to Rocq or to write a Rocq package), the remainder of this file explains how to do so. Build Requirements ------------------ -To compile Coq yourself, you need: +To compile Rocq yourself, you need: - [OCaml](https://ocaml.org/) (version >= 4.09.0) - (This version of Coq has been tested up to OCaml 4.14.1, for the 4.x series) + (This version of Rocq has been tested up to OCaml 4.14.1, for the 4.x series) Support for OCaml 5.x remains experimental. @@ -52,7 +52,7 @@ would enable proving `False` on this architecture. Note that OCaml dependencies (`zarith` and `lablgtk3-sourceview3` at this moment) must be properly registered with `findlib/ocamlfind` -since Coq's build system uses `findlib` to locate them. +since Rocq's build system uses `findlib` to locate them. Debian / Ubuntu users can get the necessary system packages for CoqIDE with: @@ -62,11 +62,11 @@ CoqIDE with: Opam (https://opam.ocaml.org/) is recommended to install OCaml and the corresponding packages. - $ opam switch create coq --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda" + $ opam switch create rocq --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda" $ eval $(opam env) $ opam install dune ocamlfind zarith lablgtk3-sourceview3 -should get you a reasonable OCaml environment to compile Coq. See the +should get you a reasonable OCaml environment to compile Rocq. See the OPAM documentation for more help. Nix users can also get all the required dependencies by running: @@ -82,12 +82,12 @@ run-time dependencies if you wish to use the native compiler. Build and install procedure --------------------------- -Note that Coq supports a faster, but less optimized developer build, +Note that Rocq supports a faster, but less optimized developer build, but final users must always use the release build. See [dev/doc/build-system.dune.md](dev/doc/build-system.dune.md) for more details. -To build and install Coq (and CoqIDE if desired) do: +To build and install Rocq (and CoqIDE if desired) do: $ ./configure -prefix $options $ make dunestrap @@ -97,7 +97,7 @@ To build and install Coq (and CoqIDE if desired) do: You can drop the `coqide` packages if not needed. Packagers may want to play with `dune install` options as to tweak -installation path, the `-prefix` argument in `./configure` tells Coq +installation path, the `-prefix` argument in `./configure` tells Rocq where to find its standard library, but doesn't control any other installation path these days. @@ -106,18 +106,18 @@ OCaml toolchain advisory When loading plugins or `vo` files, you should make sure that these were compiled with the same OCaml setup (version, flags, -dependencies...) as Coq. Distribution of pre-compiled plugins and +dependencies...) as Rocq. Distribution of pre-compiled plugins and `.vo` files is only possible if users are guaranteed to have the same -Coq version compiled with the same OCaml toolchain. An OCaml setup +Rocq version compiled with the same OCaml toolchain. An OCaml setup mismatch is the most probable cause for an `Error while loading ...: implementation mismatch on ...`. coq_environment.txt ------------------- -Coq binaries which honor environment variables, such as `ROCQLIB`, can +Rocq binaries which honor environment variables, such as `ROCQLIB`, can be seeded values for these variables by placing a text file named `coq_environment.txt` next to them. The file can contain assignments like `ROCQLIB="some path"`, that is a variable name followed by `=` and a string that follows OCaml's escaping conventions. This feature can be -used by installers of binary package to make Coq aware of its installation +used by installers of binary package to make Rocq aware of its installation path.