Drop Coq 8.14 and MC 1.15 and 1.16 support

math-comp · Jan 15, 2024 · abbb269 · abbb269
1 parent f7b8828
commit abbb269
Show file tree

Hide file tree

Showing 7 changed files with 10 additions and 215 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -15,13 +15,10 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.14'
           - 'mathcomp/mathcomp:1.17.0-coq-8.15'
           - 'mathcomp/mathcomp:1.17.0-coq-8.16'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

diff --git a/.github/workflows/nix-action-8.14.yml b/.github/workflows/nix-action-8.14.yml
diff --git a/.nix/config.nix b/.nix/config.nix
@@ -37,7 +37,6 @@
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
-  bundles."8.14".coqPackages.coq.override.version = "8.14";
   bundles."8.15".coqPackages.coq.override.version = "8.15";
   bundles."8.16".push-branches = [ "master" "hierarchy-builder" ];
   bundles."8.16".coqPackages.coq.override.version = "8.16";

diff --git a/INSTALL.md b/INSTALL.md
@@ -2,9 +2,9 @@
 
 ## Requirements
 
-- [The Coq Proof Assistant version ≥ 8.14](https://coq.inria.fr)
+- [The Coq Proof Assistant version ≥ 8.15](https://coq.inria.fr)
 - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp)
-  + except `coq-mathcomp-solvable` ≥ 1.15.0
+  + except `coq-mathcomp-solvable` ≥ 1.17.0
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
 - [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
 
@@ -71,12 +71,12 @@ 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.14.0 and MathComp 1.13.0. For other versions, update the
+With the example of Coq 8.15.0 and MathComp 1.13.0. For other versions, update the
 version numbers accordingly.
 
-1. Install Coq 8.14.0
+1. Install Coq 8.15.0
 ```
-$ opam install coq.8.14.0
+$ opam install coq.8.15.0
 ```
 2. Install the Mathematical Components
 ```

diff --git a/README.md b/README.md
@@ -33,7 +33,7 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq 8.14 to 8.18 (or dev)
+- Compatible Coq versions: Coq 8.15 to 8.18 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
   - [MathComp fingroup 1.13 or later](https://math-comp.github.io)

diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam
@@ -19,7 +19,7 @@ build: [make "-C" "theories" "-j%{jobs}%"]
 install: [make "-C" "theories" "install"]
 depends: [
   "coq-mathcomp-classical" { = version}
-  "coq-mathcomp-solvable" { (>= "1.15.0" & < "1.19~") | (= "dev") }
+  "coq-mathcomp-solvable" { (>= "1.17.0" & < "1.20~") | (= "dev") }
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
 ]

diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam
@@ -18,8 +18,8 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  "coq" { (>= "8.14" & < "8.19~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.19~") | (= "dev") }
+  "coq" { (>= "8.15" & < "8.19~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.20~") | (= "dev") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
   "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") }