Merge pull request #3354 from proux01/mathcomp-stdlib

[extra-dev] Remove Stdlib dep in mathcomp

Author: proux01

extra-dev/packages/coq-fourcolor-reals/coq-fourcolor-reals.dev/opam

@@ -0,0 +1,35 @@
+opam-version: "2.0"
+maintainer: "[email protected]"
+
+homepage: "https://github.com/coq-community/fourcolor"
+dev-repo: "git+https://github.com/coq-community/fourcolor.git"
+bug-reports: "https://github.com/coq-community/fourcolor/issues"
+license: "CECILL-B"
+
+synopsis: "Interface for real numbers used in the Four Color Theorem"
+description: """
+An axiomatization of the setoid of classical real numbers, along
+with proofs of properties such as categoricity."""
+
+build: [make "-C" "theories/reals" "-j%{jobs}%"]
+install: [make "-C" "theories/reals" "install"]
+depends: [
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
+  "coq-mathcomp-ssreflect" {>= "2.1.0"}
+  "coq-mathcomp-algebra"
+  "coq-hierarchy-builder" {>= "1.5.0"}
+]
+
+tags: [
+  "category:Mathematics/Real Calculus and Topology"
+  "keyword:real numbers"
+  "logpath:fourcolor.reals"
+]
+authors: [
+  "Georges Gonthier"
+]
+
+url {
+  src: "git+https://github.com/coq-community/fourcolor.git"
+}

extra-dev/packages/coq-fourcolor/coq-fourcolor.dev/opam

@@ -13,20 +13,18 @@ along with the theories needed to support stating and then proving the Theorem.
 This includes an axiomatization of the setoid of classical real numbers,
 basic plane topology definitions, and a theory of combinatorial hypermaps."""
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: [make "-C" "theories/proof" "-j%{jobs}%"]
+install: [make "-C" "theories/proof" "install"]
 depends: [
-  "coq" {>= "8.16"}
-  "coq-mathcomp-ssreflect" {>= "2.0"}
-  "coq-mathcomp-algebra" 
+  "coq-fourcolor-reals" {= version}
 ]
 
 tags: [
   "category:Mathematics/Combinatorics and Graph Theory"
   "keyword:Four color theorem"
   "keyword:small scale reflection"
   "keyword:Mathematical Components"
-  "logpath:fourcolor"
+  "logpath:fourcolor.proof"
 ]
 authors: [
   "Georges Gonthier"

extra-dev/packages/coq-hierarchy-builder/coq-hierarchy-builder.dev/opam

@@ -7,10 +7,14 @@ bug-reports: "https://github.com/math-comp/hierarchy-builder/issues"
 dev-repo: "git+https://github.com/math-comp/hierarchy-builder"
 
 build: [ [ make "build"]
-         [ make "test-suite" ] {with-test}
+         [ make "test-suite" ] {with-test & rocq-core:installed}
        ]
 install: [ make "install" ]
-depends: [ "coq-elpi" {>= "1.15"} "coq" {= "dev"} ]
+depends: [
+  ("coq" {>= "8.18" & < "8.20~"} & "coq-elpi" {>= "2.0"}
+  | "coq" {>= "8.20" & < "8.21~"} & "coq-elpi" {>= "2.4" | = "dev"}
+  | "rocq-core" {>= "9.0" | = "dev"} & "coq-elpi" {>= "2.4" | = "dev"})
+]
 depexts: [
   [ "wdiff" ] {os-family = "debian" & with-test}
 ]

extra-dev/packages/coq-mathcomp-classical/coq-mathcomp-classical.dev/opam

@@ -14,7 +14,8 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-C" "classical" "-j%{jobs}%"]
 install: [make "-C" "classical" "install"]
 depends: [
-  "coq" { (>= "8.19") }
+  ("coq" {>= "8.19" & < "8.21~"}
+  | "rocq-core" { (>= "9.0" & < "9.1~") | (= "dev") })
   "coq-mathcomp-ssreflect" { (>= "2.1.0") }
   "coq-mathcomp-fingroup"
   "coq-mathcomp-algebra"
@@ -25,7 +26,6 @@ depends: [
 tags: [
   "category:Mathematics/Logic/Classical logic"
   "keyword:classical logic"
-  "keyword:classical"
   "keyword:logic"
   "keyword:sets"
   "keyword:set theory"

extra-dev/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.dev/opam

@@ -4,7 +4,7 @@ maintainer: "Cyril Cohen <[email protected]>"
 homepage: "https://github.com/math-comp/finmap"
 dev-repo: "git+https://github.com/math-comp/finmap.git"
 bug-reports: "https://github.com/math-comp/finmap/issues"
-license: "CeCILL-B"
+license: "CECILL-B"
 
 synopsis: "Finite sets, finite maps, finitely supported functions"
 description: """
@@ -14,11 +14,12 @@ types). This includes support for functions with finite support and
 multisets. The library also contains a generic order and set libary,
 which will be used to subsume notations for finite sets, eventually."""
 
-build: [make "-j%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.10"}
-  "coq-mathcomp-ssreflect" {>= "1.11.0"}
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" {>= "9.0" | = "dev"})
+  "coq-mathcomp-ssreflect" { >= "2.0" | = "dev" }
 ]
 
 tags: [

extra-dev/packages/coq-mathcomp-multinomials/coq-mathcomp-multinomials.dev/opam

@@ -3,12 +3,13 @@ maintainer: "[email protected]"
 homepage: "https://github.com/math-comp/multinomials"
 bug-reports: "https://github.com/math-comp/multinomials/issues"
 dev-repo: "git+https://github.com/math-comp/multinomials.git"
-license: "CeCILL-B"
+license: "CECILL-B"
 authors: ["Pierre-Yves Strub"]
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq"                    {>= "8.16"}
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" {>= "9.0" | = "dev"})
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-bigenough" {>= "1.0"}
@@ -17,9 +18,9 @@ depends: [
 tags: [
   "keyword:multinomials"
   "keyword:monoid algebra"
-  "category:Math/Algebra/Multinomials"
-  "category:Math/Algebra/Monoid algebra"
-  "logpath:SsrMultinomials"
+  "category:Mathematics/Algebra/Multinomials"
+  "category:Mathematics/Algebra/Monoid algebra"
+  "logpath:mathcomp.multinomials"
 ]
 synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"
 url {

extra-dev/packages/coq-mathcomp-real-closed/coq-mathcomp-real-closed.dev/opam

@@ -4,7 +4,7 @@ maintainer: "Cyril Cohen <[email protected]>"
 homepage: "https://github.com/math-comp/real-closed"
 dev-repo: "git+https://github.com/math-comp/real-closed.git"
 bug-reports: "https://github.com/math-comp/real-closed/issues"
-license: "CeCILL-B"
+license: "CECILL-B"
 
 synopsis: "Mathematical Components Library on real closed fields"
 description: """
@@ -14,11 +14,12 @@ closure (including a proof of the fundamental theorem of
 algebra). It also contains a proof of decidability of the first
 order theory of real closed field, through quantifier elimination."""
 
-build: [make "-j%{jobs}%" ]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16"}
-  "coq-mathcomp-ssreflect" {>= "2.0.0"}
+  ("coq" {>= "8.18" & < "8.21~"}
+  | "rocq-core" { >= "9.0" | = "dev" })
+  "coq-mathcomp-ssreflect" {>= "2.1"}
   "coq-mathcomp-algebra"
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" {>= "1.0.0"}

extra-dev/packages/coq-mathcomp-reals-stdlib/coq-mathcomp-reals-stdlib.dev/opam

@@ -14,6 +14,8 @@ the Coq proof-assistant using the Mathematical Components library and Stdlib."""
 build: [make "-C" "reals_stdlib" "-j%{jobs}%"]
 install: [make "-C" "reals_stdlib" "install"]
 depends: [
+  ("coq" {< "8.21~"}
+  | "rocq-stdlib" { >= "9.0" | = "dev" })
   "coq-mathcomp-reals" { = version}
 ]
 

extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam

@@ -5,19 +5,39 @@ maintainer: "Mathematical Components <[email protected]>"
 homepage: "https://math-comp.github.io/"
 bug-reports: "https://github.com/math-comp/math-comp/issues"
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
-license: "CeCILL-B"
+license: "CECILL-B"
 
 build: [ make "-C" "ssreflect" "-j" "%{jobs}%" ]
 install: [ make "-C" "ssreflect" "install" ]
 depends: [
-  ( ( "coq" {>= "8.16" & < "8.17~"} & "elpi" {>= "1.16.5"} ) |
-  # The line above can be removed at the time support for 8.16 is dropped
-    ( "coq" {>= "8.17"}
-      & "elpi" {>= "1.17.0"} ) )
-  "coq-hierarchy-builder" {>= "1.5.0"}
+  ("coq" {>= "8.19" & < "8.21~"}
+  | "rocq-core" {>= "9.0" | = "dev"})
+  # Please keep the "dev" above as it is required for the coq-dev Docker images
+  "elpi" {>= "1.17.0"}
+  "coq-hierarchy-builder" { >= "1.7.0"}
 ]
 
-tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.ssreflect" ]
+tags: [
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "keyword:bigop"
+  "keyword:big operators"
+  "keyword:biomial coefficient"
+  "keyword:integer division theory"
+  "keyword:finite sets"
+  "keyword:functions with finite domain"
+  "keyword:finite graphs"
+  "keyword:quotient types"
+  "keyword:order theory"
+  "keyword:partial order"
+  "keyword:lattices"
+  "keyword:lists"
+  "keyword:ordering and sorting lists"
+  "keyword:prime numbers"
+  "keyword:tuples"
+  "keyword:bounded lists"
+  "logpath:mathcomp.ssreflect"
+]
 authors: [ "The Mathematical Components team" ]
 
 synopsis: "Small Scale Reflection"

extra-dev/packages/coq-mathcomp-tarjan/coq-mathcomp-tarjan.dev/opam

@@ -16,7 +16,8 @@ sorting with extended guarantees for acyclic graphs."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16"}
+  ("coq" {>= "8.16" & < "8.21~"}
+  | "rocq-core" { >= "9.0" | = "dev" })
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-mathcomp-fingroup" 
   "coq-hierarchy-builder" {>= "1.4.0"}