From 4b99dc5b5f1081188cd7b659ac70beadf799f7d7 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 28 Nov 2024 16:30:50 +0100 Subject: [PATCH 1/2] update mathcomp packages --- .../coq-mathcomp-algebra.2.3.0/opam | 64 +++++++++++++++++++ .../coq-mathcomp-character.2.3.0/opam | 31 +++++++++ .../coq-mathcomp-field.2.3.0/opam | 31 +++++++++ .../coq-mathcomp-fingroup.2.3.0/opam | 30 +++++++++ .../coq-mathcomp-solvable.2.3.0/opam | 30 +++++++++ .../coq-mathcomp-ssreflect.2.3.0/opam | 54 ++++++++++++++++ 6 files changed, 240 insertions(+) create mode 100644 released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.3.0/opam create mode 100644 released/packages/coq-mathcomp-character/coq-mathcomp-character.2.3.0/opam create mode 100644 released/packages/coq-mathcomp-field/coq-mathcomp-field.2.3.0/opam create mode 100644 released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.3.0/opam create mode 100644 released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.3.0/opam create mode 100644 released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam diff --git a/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.3.0/opam b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.3.0/opam new file mode 100644 index 000000000..6a7ee93c4 --- /dev/null +++ b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.2.3.0/opam @@ -0,0 +1,64 @@ +opam-version: "2.0" +maintainer: "Mathematical Components " + +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" + +build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/algebra" "install" ] +depends: [ "coq-mathcomp-fingroup" { = version } ] + +tags: [ + "keyword:small scale reflection" + "keyword:mathematical components" + "keyword:algebra" + "keyword:algebraic structure hierarchies" + "keyword:archimedean field" + "keyword:floor" + "keyword:ceil" + "keyword:intervals" + "keyword:matrices" + "keyword:vectors" + "keyword:block matrices" + "keyword:determinant" + "keyword:Cramer rule" + "keyword:Vandermonde matrices" + "keyword:LUP decomposition" + "keyword:Gaussian elimination" + "keyword:matrix rank" + "keyword:eigen values" + "keyword:single variable polynomials" + "keyword:bivariate polynomials" + "keyword:polynomial division" + "keyword:integers" + "keyword:rational numbers" + "keyword:semirings" + "keyword:rings" + "keyword:left algebra" + "keyword:left module" + "keyword:unit rings" + "keyword:field" + "keyword:algebraically closed field" + "keyword:additive morphisms" + "keyword:ring morphisms" + "keyword:finite dimensional vector spaces" + "keyword:complex numbers" + "keyword:square root" + "logpath:mathcomp.algebra" +] +authors: [ "The Mathematical Components team" ] + +synopsis: "Mathematical Components Library on Algebra" +description: """ +This library contains definitions and theorems about discrete +(i.e. with decidable equality) algebraic structures : ring, fields, +ordered fields, real fields, modules, algebras, integers, rational +numbers, polynomials, matrices, vector spaces... +""" + +url { +src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz" +checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec" +} diff --git a/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.3.0/opam b/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.3.0/opam new file mode 100644 index 000000000..4a278df39 --- /dev/null +++ b/released/packages/coq-mathcomp-character/coq-mathcomp-character.2.3.0/opam @@ -0,0 +1,31 @@ +opam-version: "2.0" +maintainer: "Mathematical Components " + +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" + +build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/character" "install" ] +depends: [ "coq-mathcomp-field" { = version } ] + +tags: [ + "keyword:small scale reflection" + "keyword:mathematical components" + "keyword:algebra" + "keyword:character" + "logpath:mathcomp.character" +] +authors: [ "The Mathematical Components team" ] + +synopsis: "Mathematical Components Library on character theory" +description:""" +This library contains definitions and theorems about group +representations, characters and class functions. +""" + +url { +src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz" +checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec" +} diff --git a/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.3.0/opam b/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.3.0/opam new file mode 100644 index 000000000..1f0fff5e0 --- /dev/null +++ b/released/packages/coq-mathcomp-field/coq-mathcomp-field.2.3.0/opam @@ -0,0 +1,31 @@ +opam-version: "2.0" +maintainer: "Mathematical Components " + +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" + +build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/field" "install" ] +depends: [ "coq-mathcomp-solvable" { = version } ] + +tags: [ + "keyword:small scale reflection" + "keyword:mathematical components" + "keyword:algebra" + "keyword:field" + "logpath:mathcomp.field" +] +authors: [ "The Mathematical Components team" ] + +synopsis: "Mathematical Components Library on Fields" +description:""" +This library contains definitions and theorems about field extensions, +galois theory, algebraic numbers, cyclotomic polynomials... +""" + +url { +src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz" +checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec" +} diff --git a/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.3.0/opam b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.3.0/opam new file mode 100644 index 000000000..b1146d8d7 --- /dev/null +++ b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.2.3.0/opam @@ -0,0 +1,30 @@ +opam-version: "2.0" +maintainer: "Mathematical Components " + +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" + +build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/fingroup" "install" ] +depends: [ "coq-mathcomp-ssreflect" { = version } ] + +tags: [ + "keyword:small scale reflection" + "keyword:mathematical components" + "keyword:finite groups" + "logpath:mathcomp.fingroup" +] +authors: [ "The Mathematical Components team" ] + +synopsis: "Mathematical Components Library on finite groups" +description: """ +This library contains definitions and theorems about finite groups, +group quotients, group morphisms, group presentation, group action... +""" + +url { +src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz" +checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec" +} diff --git a/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.3.0/opam b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.3.0/opam new file mode 100644 index 000000000..82d6c00b8 --- /dev/null +++ b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.2.3.0/opam @@ -0,0 +1,30 @@ +opam-version: "2.0" +maintainer: "Mathematical Components " + +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" + +build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/solvable" "install" ] +depends: [ "coq-mathcomp-algebra" { = version } ] + +tags: [ + "keyword:small scale reflection" + "keyword:mathematical components" + "keyword:finite groups" + "logpath:mathcomp.solvable" +] +authors: [ "The Mathematical Components team" ] + +synopsis: "Mathematical Components Library on finite groups (II)" + +description:""" +This library contains more definitions and theorems about finite groups. +""" + +url { +src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz" +checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec" +} diff --git a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam new file mode 100644 index 000000000..7dd1712eb --- /dev/null +++ b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam @@ -0,0 +1,54 @@ +opam-version: "2.0" +maintainer: "Mathematical Components " + +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" + +build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ] +install: [ make "-C" "mathcomp/ssreflect" "install" ] +depends: [ + "coq" {(>= "8.18" & < "8.21~") | (= "dev")} + # Please keep the "dev" above as it is required for the coq-dev Docker images + "elpi" {>= "1.17.0"} + "coq-hierarchy-builder" { >= "1.5.0"} +] + +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" +description: """ +This library includes the small scale reflection proof language +extension and the minimal set of libraries to take advantage of it. +This includes libraries on lists (seq), boolean and boolean +predicates, natural numbers and types with decidable equality, +finite types, finite sets, finite functions, finite graphs, basic arithmetics +and prime numbers, big operators +""" + +url { +src: "https://github.com/math-comp/math-comp/archive/mathcomp-2.3.0.tar.gz" +checksum: "sha256=19e13c8765007f95b4656d8902bc66e10b072ab94ab51031c5efb860827d05ec" +} From b2bc2ec299cca1020134f5ee382214aa8122e0ae Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Fri, 29 Nov 2024 09:12:39 +0100 Subject: [PATCH 2/2] Update released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam --- .../coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam index 7dd1712eb..472f5d178 100644 --- a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam +++ b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.2.3.0/opam @@ -12,7 +12,7 @@ depends: [ "coq" {(>= "8.18" & < "8.21~") | (= "dev")} # Please keep the "dev" above as it is required for the coq-dev Docker images "elpi" {>= "1.17.0"} - "coq-hierarchy-builder" { >= "1.5.0"} + "coq-hierarchy-builder" { >= "1.7.0"} ] tags: [