Merge pull request #31 from coq-community/release-1.17

update packages and CI for MathComp up to and including 1.17.0

Author: palmskog

.github/workflows/docker-action.yml

@@ -17,7 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'

coq-graph-theory-planar.opam

@@ -15,8 +15,8 @@ as part of the Coq proof of the Four-Color Theorem."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "coq" {(>= "8.14" & < "8.17~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.13" & < "1.16~") | (= "dev")}
+  "coq" {(>= "8.14" & < "8.18~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "1.18~"}
   "coq-graph-theory" {= version}
   "coq-fourcolor"
 ]

coq-graph-theory.opam

@@ -16,8 +16,8 @@ from the literature (e.g., Menger's Theorem and Hall's Marriage Theorem)."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
-  "coq" {(>= "8.14" & < "8.17~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.13" & < "1.16~") | (= "dev")}
+  "coq" {(>= "8.14" & < "8.18~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {>= "1.13" & < "1.18~"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-finmap" 
   "coq-hierarchy-builder" {>= "1.1.0"}

depopts.patch

@@ -65,11 +65,15 @@ license:
 
 supported_coq_versions:
   text: 8.14 or later
-  opam: '{(>= "8.14" & < "8.17~") | (= "dev")}'
+  opam: '{(>= "8.14" & < "8.18~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
+- version: '1.17.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '1.16.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '1.15.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
@@ -82,7 +86,7 @@ ci_cron_schedule: '25 5 * * 5'
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.13" & < "1.16~") | (= "dev")}'
+    version: '{>= "1.13" & < "1.18~"}'
   description: MathComp's [SSReflect library](https://math-comp.github.io), version 1.13 or later
 - opam:
     name: coq-mathcomp-algebra