From 636c5d4f9aa6998f623ceb7f8eb634d3c1353015 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 7 Jan 2024 17:38:20 +0100
Subject: [PATCH] adjust opam packages and ci for MathComp 1.18 and other
 changes

---
 .github/workflows/docker-action.yml |  2 +-
 coq-addition-chains.opam            |  4 ++--
 coq-gaia-hydras.opam                |  4 ++--
 coq-goedel.opam                     |  2 +-
 coq-hydra-battles.opam              |  2 +-
 meta.yml                            | 16 +++++++++-------
 6 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 52f4ada8..ad280f90 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -15,6 +15,7 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.18.0-coq-8.18'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
           - 'mathcomp/mathcomp:1.15.0-coq-8.16'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
@@ -27,7 +28,6 @@ jobs:
           custom_image: ${{ matrix.image }}
           custom_script: |
             startGroup "Setup and print opam config"
-              opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
               opam config list; opam repo list; opam list
             endGroup
             startGroup "Build hydra-battles dependencies"
diff --git a/coq-addition-chains.opam b/coq-addition-chains.opam
index 4b02fc2d..b94853ba 100644
--- a/coq-addition-chains.opam
+++ b/coq-addition-chains.opam
@@ -18,8 +18,8 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
-  "coq-paramcoq" {(>= "1.1.3" & < "1.2~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"}
+  "coq-paramcoq" {>= "1.1.3"}
+  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
   "coq-mathcomp-algebra"
 ]
 
diff --git a/coq-gaia-hydras.opam b/coq-gaia-hydras.opam
index e4b5c505..14cee304 100644
--- a/coq-gaia-hydras.opam
+++ b/coq-gaia-hydras.opam
@@ -18,9 +18,9 @@ depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
   "coq-hydra-battles" {= version}
-  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.18"}
+  "coq-mathcomp-ssreflect" {>= "1.13.0" & < "1.19"}
   "coq-mathcomp-zify" {< "2"}
-  "coq-gaia-schutte" {>= "1.14" & < "1.18~"}
+  "coq-gaia-schutte" {>= "1.14" & < "1.18"}
 ]
 
 tags: [
diff --git a/coq-goedel.opam b/coq-goedel.opam
index 5a216e54..b4a48e18 100644
--- a/coq-goedel.opam
+++ b/coq-goedel.opam
@@ -18,7 +18,7 @@ depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
   "coq-hydra-battles" {= version}
-  "coq-coqprime" {= "dev"}
+  "coq-coqprime" {>= "1.2.0"}
 ]
 
 tags: [
diff --git a/coq-hydra-battles.opam b/coq-hydra-battles.opam
index 10d631a5..07b7dd64 100644
--- a/coq-hydra-battles.opam
+++ b/coq-hydra-battles.opam
@@ -19,7 +19,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
   "coq" {>= "8.14"}
-  "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
+  "coq-equations" {>= "1.2"}
   "coq-zorns-lemma" {>= "10.2.0"}
   "coq-libhyps"
 ]
diff --git a/meta.yml b/meta.yml
index 51ff87e0..d4d920ed 100644
--- a/meta.yml
+++ b/meta.yml
@@ -120,6 +120,8 @@ supported_coq_versions:
   opam: '{>= "8.14"}'
 
 tested_coq_opam_versions:
+- version: '1.18.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 - version: '1.17.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '1.15.0-coq-8.16'
@@ -132,28 +134,28 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-equations
-    version: '{(>= "1.2" & < "1.4~") | (= "dev")}'
+    version: '{>= "1.2"}'
   description: |-
     [Equations](https://github.com/mattam82/Coq-Equations) 1.2 or later
 - opam:
     name: coq-paramcoq
-    version: '{(>= "1.1.3" & < "1.2~") | (= "dev")}'
+    version: '{>= "1.1.3"}'
   description: |-
     [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.13.0" & < "1.18~")}'
+    version: '{>= "1.13.0" & < "1.19"}'
   description: |-
-    [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 or later
+    [MathComp SSReflect](https://github.com/math-comp/math-comp) 1.13 to 1.18
 - opam:
     name: coq-mathcomp-algebra
   description: |-
     [MathComp Algebra](https://github.com/math-comp/math-comp)
 - opam:
     name: coq-gaia-schutte
-    version: '{(>= "1.14" & < "1.18~") | (= "dev")}'
+    version: '{>= "1.14" & < "1.18"}'
   description: |-
-    [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 or later
+    [Gaia's Schütte ordinals](https://github.com/coq-community/gaia) 1.14 to 1.17
 - opam:
     name: coq-mathcomp-zify
     version: '{< "2~"}'
@@ -165,7 +167,7 @@ dependencies:
     [LibHyps](https://github.com/Matafou/LibHyps)
 - opam:
     name: coq-coqprime
-    version: '{= "dev"}'
+    version: '{>= "1.2.0"}'
   description: |-
     [CoqPrime](https://github.com/thery/coqprime)
 - opam: