Merge pull request #81 from coq-community/meta-deps-8.19

explicitly record implicit dependencies, update boilerplate for 8.18

.github/workflows/docker-action.yml

@@ -17,6 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
           - 'mathcomp/mathcomp:2.0.0-coq-8.17'
           - 'mathcomp/mathcomp:2.0.0-coq-8.16'
       fail-fast: false
@@ -26,11 +28,6 @@ jobs:
         with:
           opam_file: 'coq-coqeal.opam'
           custom_image: ${{ matrix.image }}
-          before_install: |
-            startGroup "Add extra-dev repo"
-              opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-              opam config list; opam repo list; opam list
-            endGroup
 
 
 # See also:

README.md

@@ -48,9 +48,11 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
 - Additional dependencies:
   - [Bignums](https://github.com/coq/bignums) same version as Coq
   - [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
-  - [MathComp Multinomials](https://github.com/math-comp/multinomials) >= 2.0 or later
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
+  - [MathComp ssreflect](https://math-comp.github.io) 2.0 or later
   - [MathComp algebra](https://math-comp.github.io) 2.0 or later
-  - [MathComp real-closed](https://math-comp.github.io) 1.1.2 or later
+  - [MathComp Multinomials](https://github.com/math-comp/multinomials) 2.0 or later
+  - [MathComp real-closed](https://math-comp.github.io) 2.0 or later
 - Coq namespace: `CoqEAL`
 - Related publication(s):
   - [A refinement-based approach to computational algebra in Coq](https://hal.inria.fr/hal-00734505/document) doi:[10.1007/978-3-642-32347-8_7](https://doi.org/10.1007/978-3-642-32347-8_7)

coq-coqeal.opam

@@ -21,12 +21,14 @@ of the ForMath EU FP7 project (2009-2013). It has two parts:
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.18~") | (= "dev")}
+  "coq" {(>= "8.16" & < "8.19~") | (= "dev")}
   "coq-bignums" 
   "coq-paramcoq" {>= "1.1.3"}
-  "coq-mathcomp-multinomials" {((>= "2.0" & < "2.1~") | = "dev")}
-  "coq-mathcomp-algebra" {((>= "2.0" & < "2.1~") | = "dev")}
-  "coq-mathcomp-real-closed" {(= "dev")}
+  "coq-hierarchy-builder" {>= "1.4.0"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-multinomials" {>= "2.0"}
+  "coq-mathcomp-real-closed" {>= "2.0"}
 ]
 
 tags: [

meta.yml

@@ -77,7 +77,7 @@ license:
 
 supported_coq_versions:
   text: 8.16 or later (use releases for other Coq versions)
-  opam: '{(>= "8.16" & < "8.18~") | (= "dev")}'
+  opam: '{(>= "8.16" & < "8.19~") | (= "dev")}'
 
 dependencies:
 - opam:
@@ -90,22 +90,35 @@ dependencies:
   description: |-
     [Paramcoq](https://github.com/coq-community/paramcoq) 1.1.3 or later
 - opam:
-    name: coq-mathcomp-multinomials
-    version: '{((>= "2.0" & < "2.1~") | = "dev")}'
+    name: coq-hierarchy-builder
+    version: '{>= "1.4.0"}'
+  description: |-
+    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
+- opam:
+    name: coq-mathcomp-ssreflect
+    version: '{>= "2.0"}'
   description: |-
-    [MathComp Multinomials](https://github.com/math-comp/multinomials) >= 2.0 or later
+    [MathComp ssreflect](https://math-comp.github.io) 2.0 or later
 - opam:
     name: coq-mathcomp-algebra
-    version: '{((>= "2.0" & < "2.1~") | = "dev")}'
   description: |-
     [MathComp algebra](https://math-comp.github.io) 2.0 or later
+- opam:
+    name: coq-mathcomp-multinomials
+    version: '{>= "2.0"}'
+  description: |-
+    [MathComp Multinomials](https://github.com/math-comp/multinomials) 2.0 or later
 - opam:
     name: coq-mathcomp-real-closed
-    version: '{(= "dev")}'
+    version: '{>= "2.0"}'
   description: |-
-    [MathComp real-closed](https://math-comp.github.io) 1.1.2 or later
+    [MathComp real-closed](https://math-comp.github.io) 2.0 or later
 
 tested_coq_opam_versions:
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
+- version: '2.0.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '2.0.0-coq-8.16'