cleanup README / INSTALL instructions (#1619)

Author: hoheinzollern

INSTALL.md

@@ -2,16 +2,16 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.20](https://coq.inria.fr)
+- [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org)
 - [Mathematical Components version ≥ 2.2.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap)
-- [Hierarchy builder version >= 1.7.0](https://github.com/math-comp/hierarchy-builder)
-- [bigenough >= 1.0.0](https://github.com/math-comp/bigenough)
+- [Hierarchy builder version ≥ 1.7.0](https://github.com/math-comp/hierarchy-builder)
+- [bigenough ≥ 1.0.0](https://github.com/math-comp/bigenough)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
-the repository https://coq.inria.fr/opam/released, which you can add by typing
-`opam repo add coq-released https://coq.inria.fr/opam/released`.
+the repository https://rocq-prover.org/opam/released, which you can add by typing
+`opam repo add rocq-released https://rocq-prover.org/opam/released`.
 
 Detailed instructions for possible installations of Mathematical Components are located
 [here](https://github.com/math-comp/math-comp/blob/master/INSTALL.md).
@@ -22,8 +22,10 @@ Detailed instructions for possible installations of Mathematical Components are
   + type `opam install coq-mathcomp-analysis.X.Y.Z` where `X.Y.Z` is the version number
     (all the dependencies should be automatically installed, assuming `opam` has been properly
     configured and `coq-released` repository is added)
-- Custom (assuming the requirements are met):
-  + type `make` to use the provided `Makefile`
+- Custom:
+  + first, install the required dependencies, for example with opam
+    type `opam install --deps-only coq-mathcomp-analysis.X.Y.Z`
+  + assuming the requirements are met, type `make` to use the provided `Makefile`
 
 ## From scratch instructions
 
@@ -40,7 +42,7 @@ $ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/instal
 $ export OPAMROOT=~/.opam_mathcomp_analysis # opam configuration, metadata, logs, temporary directories and caches
 $ opam init -j4 # adapt to the number of cores you have
 $ eval `opam config env`
-$ opam repo add coq-released https://coq.inria.fr/opam/released
+$ opam repo add rocq-released https://rocq-prover.org/opam/released
 ```
 3. Install our package (and all its dependencies)
 ```
@@ -71,7 +73,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.20.0 and MathComp 2.3.0. For other versions, update the
+With the example of Coq 8.20.1 and MathComp 2.3.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.20.1

README.md

@@ -1,7 +1,3 @@
-<!---
-This file was generated from `meta.yml`, please do not edit manually.
-Follow the instructions on https://github.com/coq-community/templates to regenerate.
---->
 # Analysis library compatible with Mathematical Components
 
 [![Nix CI][nix-action-shield]][nix-action-link]
@@ -11,9 +7,9 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [nix-action-link]: https://github.com/math-comp/analysis/actions?query=branch%3Amaster+event%3Apush
 
 [chat-shield]: https://img.shields.io/badge/zulip-join_chat-brightgreen.svg
-[chat-link]: https://coq.zulipchat.com/login/#narrow/stream/237666-math-comp-analysis
+[chat-link]: https://rocq-prover.zulipchat.com/#narrow/channel/237666-math-comp-analysis
 
-This repository contains a real analysis library for the Coq proof-assistant.
+This repository contains a real analysis library for the Coq / Rocq proof-assistant.
 It is based on the [Mathematical Components](https://math-comp.github.io/) library.
 
 In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the following packages:
@@ -46,7 +42,7 @@ The easiest way to install the latest released version of MathComp-Analysis libr
 via the [opam](https://opam.ocaml.org/doc/Install.html) package manager:
 
 ```shell
-opam repo add coq-released https://coq.inria.fr/opam/released
+opam repo add rocq-released https://rocq-prover.org/opam/released
 opam install coq-mathcomp-analysis
 ```
 Note that the packages `coq-mathcomp-classical` and `coq-mathcomp-reals` will be installed as dependencies.
@@ -58,7 +54,7 @@ To build and install manually, make sure that the dependencies are met and do:
 ``` shell
 git clone https://github.com/math-comp/analysis.git
 cd analysis
-make   # or make -j <number-of-cores-on-your-machine> 
+make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```