Require MC >= 2.4.0

Author: proux01

.github/workflows/nix-action-8.20-2.3.0.yml

@@ -52,11 +52,6 @@ in {
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
 
-  bundles."8.20-2.3.0".coqPackages = common-bundle // {
-    coq.override.version = "8.20";
-    mathcomp.override.version = "2.3.0";
-  };
-
   bundles."8.20-2.4.0".coqPackages = common-bundle // {
     coq.override.version = "8.20";
     mathcomp.override.version = "2.4.0";

.nix/config.nix

@@ -80,6 +80,11 @@
 
 ### Removed
 
+- file `interval_inference.v` (now in MathComp)
+
+- in file `all_reals.v`
+  + export of `interval_inference` (now in mathcomp-algebra, but not automatically exported)
+
 ### Infrastructure
 
 ### Misc

CHANGELOG_UNRELEASED.md

@@ -3,7 +3,7 @@
 ## Requirements
 
 - [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org)
-- [Mathematical Components version ≥ 2.3.0](https://github.com/math-comp/math-comp)
+- [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)
 - [bigenough ≥ 1.0.0](https://github.com/math-comp/bigenough)
@@ -73,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.1 and MathComp 2.3.0. For other versions, update the
+With the example of Coq 8.20.1 and MathComp 2.4.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.20.1
@@ -82,11 +82,11 @@ $ opam install coq.8.20.1
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.2.3.0
-$ opam install coq-mathcomp-fingroup.2.3.0
-$ opam install coq-mathcomp-algebra.2.3.0
-$ opam install coq-mathcomp-solvable.2.3.0
-$ opam install coq-mathcomp-field.2.3.0
+$ 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
 ```
 3. Install the Finite maps library
 ```

INSTALL.md

@@ -45,25 +45,6 @@ all: config build
 .PHONY: pre-makefile
 
 Makefile.coq: pre-makefile $(COQPROJECT) Makefile
-	(echo "From mathcomp.algebra Require Import interval_inference." > test_interval_inference.v \
-	 && ($(COQC) test_interval_inference.v > /dev/null 2>&1) \
-	 && test -f interval_inference.v -o -f reals/interval_inference.v \
-	 && touch rm_interval_inference) || true
-	$(RM) test_interval_inference.v
-	test -f rm_interval_inference \
-	  && sed -i.bak '/interval_inference/ d' $(COQPROJECT) \
-	  && $(RM) $(COQPROJECT).bak || true
-	test -f rm_interval_inference \
-	  && sed -i.bak '/interval_inference/ d' all_reals.v \
-	  && $(RM) all_reals.v.bak || true
-	test -f rm_interval_inference \
-	  && sed -i.bak '/interval_inference/ d' reals/all_reals.v \
-	  && $(RM) reals/all_reals.v.bak || true
-	test -f rm_interval_inference && $(RM) interval_inference.v || true
-	test -f rm_interval_inference && $(RM) reals/interval_inference.v || true
-	$(RM) rm_interval_inference
-	# Remove everything above when requiring mathcomp >= 2.4.0
-	# (also remove file reals/interval_inference.v and references to it)
 	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
 
 # Global config, build, clean and distclean --------------------------
@@ -142,6 +123,5 @@ html: build $(DOCDIR)/dependency_graph.dot
 	-hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \
         -index-blacklist etc/rocqnavi_index-blacklist \
         -show-type-information-using-coqtop-process \
-	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.ssreflect \
-	-external https://math-comp.github.io/htmldoc_2_3_0/ mathcomp.algebra
-
+	-external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.ssreflect \
+	-external https://math-comp.github.io/htmldoc_2_4_0/ mathcomp.algebra

Makefile.common

@@ -26,11 +26,11 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol
 - License: [CeCILL-C](LICENSE)
 - Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev)
 - Additional dependencies:
-  - [MathComp ssreflect 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp fingroup 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp algebra 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp solvable 2.3.0 or later](https://math-comp.github.io)
-  - [MathComp field 2.3.0 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp fingroup 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp solvable 2.4.0 or later](https://math-comp.github.io)
+  - [MathComp field 2.4.0 or later](https://math-comp.github.io)
   - [MathComp finmap 2.1.0](https://github.com/math-comp/finmap)
   - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
   - [Hierarchy Builder 1.8.0 or later](https://github.com/math-comp/hierarchy-builder)

README.md

@@ -30,7 +30,6 @@ reals/constructive_ereal.v
 reals/reals.v
 reals/real_interval.v
 reals/signed.v
-reals/interval_inference.v
 reals/prodnormedzmodule.v
 reals/all_reals.v
 experimental_reals/xfinmap.v

_CoqProject

@@ -17,7 +17,7 @@ install: [make "-C" "classical" "install"]
 depends: [
   ("coq" {>= "8.20" & < "8.21~"}
   | "coq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
-  "coq-mathcomp-ssreflect" { (>= "2.3.0" & < "2.5~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.5~") | (= "dev") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
   "coq-mathcomp-finmap" { (>= "2.1.0") }

coq-mathcomp-classical.opam

@@ -11,6 +11,5 @@ constructive_ereal.v
 reals.v
 real_interval.v
 signed.v
-interval_inference.v
 prodnormedzmodule.v
 all_reals.v

reals/Make

@@ -1,4 +1,3 @@
-From mathcomp Require Export interval_inference.
 From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export reals.
 From mathcomp Require Export real_interval.