Drop support for Coq 8.20

Author: proux01

…thub/workflows/nix-action-8.20-2.4.0.yml …ithub/workflows/nix-action-9.0-2.4.0.yml.github/workflows/nix-action-8.20-2.4.0.yml renamed to .github/workflows/nix-action-9.0-2.4.0.yml .github/workflows/nix-action-8.20-2.4.0.yml renamed to .github/workflows/nix-action-9.0-2.4.0.yml

@@ -53,10 +53,14 @@ in {
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
 
-  bundles."8.20-2.4.0".coqPackages = common-bundle // {
-    coq.override.version = "8.20";
-    mathcomp.override.version = "2.4.0";
-    mathcomp-infotheo.job = false;
+  bundles."9.0-2.4.0" = {
+    rocqPackages = {
+      rocq-core.override.version = "9.0";
+    };
+    coqPackages = common-bundle // {
+      coq.override.version = "9.0";
+      mathcomp.override.version = "2.4.0";
+    };
   };
 
   bundles."9.0" = {

.nix/config.nix

@@ -2,7 +2,7 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org)
+- [The Rocq Prover version ≥ 9.0](https://rocq-prover.org)
 - [Mathematical Components version ≥ 2.4.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap)
 - [Hierarchy builder version ≥ 1.8.0](https://github.com/math-comp/hierarchy-builder)
@@ -73,28 +73,28 @@ 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.1 and MathComp 2.4.0. For other versions, update the
+With the example of Coq 9.1.1 and MathComp 2.5.0. For other versions, update the
 version numbers accordingly.
 
-1. Install Coq 8.20.1
+1. Install Rocq 9.1.1
 ```
-$ opam install coq.8.20.1
+$ opam install rocq-core.9.1.1
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.2.4.0
-$ opam install coq-mathcomp-fingroup.2.4.0
-$ opam install coq-mathcomp-algebra.2.4.0
-$ opam install coq-mathcomp-solvable.2.4.0
-$ opam install coq-mathcomp-field.2.4.0
+$ opam install rocq-mathcomp-ssreflect.2.5.0
+$ opam install rocq-mathcomp-fingroup.2.5.0
+$ opam install rocq-mathcomp-algebra.2.5.0
+$ opam install rocq-mathcomp-solvable.2.5.0
+$ opam install rocq-mathcomp-field.2.5.0
 ```
 3. Install the Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.2.2.0
+$ opam install rocq-mathcomp-finmap.2.2.0
 ```
 4. Install the Hierarchy Builder
 ```
-$ opam install coq-hierarchy-builder.1.8.0
+$ opam install rocq-hierarchy-builder.1.10.2
 ```
 5. Download and compile `coq-mathcomp-analysis` without installing
 ```

INSTALL.md

@@ -113,7 +113,7 @@ html: build $(DOCDIR)/dependency_graph.dot
 	-Q reals_stdlib mathcomp.reals_stdlib \
 	-Q experimental_reals mathcomp.experimental_reals \
 	-Q analysis_stdlib mathcomp.analysis_stdlib \
-	-coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \
+	-coqlib https://rocq-prover.org/doc/V9.0.0/stdlib/ \
 	-dependency-graph $(DOCDIR)/dependency_graph.dot \
 	-hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \
         -index-blacklist etc/rocqnavi_index-blacklist \

Makefile.common

@@ -24,7 +24,7 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol
 
 - [Authors](AUTHORS.md)
 - License: [CeCILL-C](LICENSE)
-- Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev)
+- Compatible Rocq versions: Rocq 9.0 and 9.1 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 2.4.0 or later](https://math-comp.github.io)
   - [MathComp fingroup 2.4.0 or later](https://math-comp.github.io)

Makefile.coq.local

@@ -9,7 +9,14 @@ license: "CECILL-C"
 
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
-depends: [ "rocq-mathcomp-classical" { = version} ]
+depends: [
+  "coq-core" { (>= "9.0" & < "9.2~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
+  "coq-mathcomp-fingroup"
+  "coq-mathcomp-algebra"
+  "coq-mathcomp-finmap" { (>= "2.1.0") }
+  "coq-hierarchy-builder" { (>= "1.8.0") }
+]
 
 tags: [
   "category:Mathematics/Logic/Classical logic"