Merge pull request #123 from proux01/rocq

Compat with Rocq (without coq shim)

Author: proux01

.github/workflows/docker-action.yml

@@ -32,7 +32,7 @@ jobs:
       - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-mathcomp-multinomials.opam'
+          opam_file: 'rocq-mathcomp-multinomials.opam'
           custom_image: ${{ matrix.image }}
 
 

Makefile

@@ -6,10 +6,12 @@ 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
-	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+	$(COQMAKEFILE) -f _CoqProject -o Makefile.coq
 
 invoke-coqmakefile: Makefile.coq
 	$(MAKE) --no-print-directory -f Makefile.coq $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))

coq-mathcomp-multinomials.opam

@@ -10,30 +10,6 @@ dev-repo: "git+https://github.com/math-comp/multinomials.git"
 bug-reports: "https://github.com/math-comp/multinomials/issues"
 license: "CECILL-B"
 
-synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
-description: """
-This library provides a library for monomial algebra, for multivariate
-polynomials over ring structures and an extended theory for polynomials whose
-coefficients range over commutative rings and integral domains."""
+depends: [ "rocq-mathcomp-multinomials" { = version } ]
 
-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" 
-  "coq-mathcomp-bigenough" 
-  "coq-mathcomp-finmap" 
-]
-
-tags: [
-  "category:Mathematics/Algebra/Multinomials"
-  "category:Mathematics/Algebra/Monoid algebra"
-  "keyword:multinomials"
-  "keyword:monoid algebra"
-  "logpath:mathcomp.multinomials"
-]
-authors: [
-  "Pierre-Yves Strub"
-]
+synopsis: "Compatibility package for rocq-mathcomp-multinomials"

rocq-mathcomp-multinomials.opam

@@ -0,0 +1,37 @@
+opam-version: "2.0"
+maintainer: "pierre-yves@strub.nu"
+version: "dev"
+
+homepage: "https://github.com/math-comp/multinomials"
+dev-repo: "git+https://github.com/math-comp/multinomials.git"
+bug-reports: "https://github.com/math-comp/multinomials/issues"
+license: "CECILL-B"
+
+synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
+description: """
+This library provides a library for monomial algebra, for multivariate
+polynomials over ring structures and an extended theory for polynomials whose
+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" 
+  "coq-mathcomp-bigenough" 
+  "coq-mathcomp-finmap" 
+]
+conflicts: [ "coq-mathcomp-multinomials" {<= "2.4.0"} ]
+
+tags: [
+  "category:Mathematics/Algebra/Multinomials"
+  "category:Mathematics/Algebra/Monoid algebra"
+  "keyword:multinomials"
+  "keyword:monoid algebra"
+  "logpath:mathcomp.multinomials"
+]
+authors: [
+  "Pierre-Yves Strub"
+]