Merge pull request #124 from math-comp/meta_yml

Update meta.yml and require Rocq 9.0

Author: pi8027

.github/workflows/docker-action.yml

@@ -18,10 +18,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.4.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.1'
-          - 'mathcomp/mathcomp:2.5.0-coq-8.20'
           - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
           - 'mathcomp/mathcomp-dev:rocq-prover-9.0'

Makefile

@@ -6,12 +6,10 @@ KNOWNTARGETS := Makefile.coq
 # on them always get rebuilt
 KNOWNFILES   := Makefile _CoqProject
 
-COQMAKEFILE?=$(shell command -v coq_makefile || echo "$(COQBIN)rocq makefile")
-
 .DEFAULT_GOAL := invoke-coqmakefile
 
 Makefile.coq: Makefile _CoqProject
-	$(COQMAKEFILE) -f _CoqProject -o Makefile.coq
+	$(COQBIN)rocq makefile -f _CoqProject -o Makefile.coq
 
 invoke-coqmakefile: Makefile.coq
 	$(MAKE) --no-print-directory -f Makefile.coq $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))

README.md

@@ -21,7 +21,7 @@ coefficients range over commutative rings and integral domains.
 - Author(s):
   - Pierre-Yves Strub (initial)
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Rocq/Coq versions: 8.20 or later
+- Compatible Rocq/Coq versions: 9.0 or later
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) ssreflect 2.4 or later
   - [MathComp](https://math-comp.github.io) algebra
@@ -37,7 +37,7 @@ is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
 opam repo add rocq-released https://rocq-prover.org/opam/released
-opam install coq-mathcomp-multinomials
+opam install rocq-mathcomp-multinomials
 ```
 
 To instead build and install manually, you need to make sure that all the

coq-mathcomp-multinomials.opam

@@ -1,6 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
 maintainer: "pierre-yves@strub.nu"
 version: "dev"

meta.yml

@@ -1,7 +1,7 @@
 ---
 fullname: A Multivariate polynomial Library for the Mathematical Components Library
 shortname: multinomials
-opam_name: coq-mathcomp-multinomials
+opam_name: rocq-mathcomp-multinomials
 organization: math-comp
 action: true
 
@@ -25,20 +25,16 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.20 or later
-  opam: '{>= "8.20"}'
+  text: 9.0 or later
+  opam: '{>= "9.0"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- version: '2.4.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-9.1'
   repo: 'mathcomp/mathcomp'
-- version: '2.5.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.5.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 - version: '2.5.0-rocq-prover-9.1'
@@ -52,12 +48,12 @@ tested_coq_opam_versions:
 
 dependencies:
 - opam:
-    name: coq-mathcomp-ssreflect
+    name: rocq-mathcomp-ssreflect
     version: '{>= "2.4"}'
   description: |-
     [MathComp](https://math-comp.github.io) ssreflect 2.4 or later
 - opam:
-    name: coq-mathcomp-algebra
+    name: rocq-mathcomp-algebra
   description: |-
     [MathComp](https://math-comp.github.io) algebra
 - opam:

rocq-mathcomp-multinomials.opam

@@ -1,3 +1,6 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
 opam-version: "2.0"
 maintainer: "pierre-yves@strub.nu"
 version: "dev"
@@ -16,10 +19,9 @@ coefficients range over commutative rings and integral domains."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  ("coq" {>= "8.20" & < "8.21~"}
-  | "rocq-core" {>= "9.0"})
-  "coq-mathcomp-ssreflect" {>= "2.4"}
-  "coq-mathcomp-algebra" 
+  "rocq-core" {>= "9.0"}
+  "rocq-mathcomp-ssreflect" {>= "2.4"}
+  "rocq-mathcomp-algebra" 
   "coq-mathcomp-bigenough" 
   "coq-mathcomp-finmap" 
 ]