From 3ca9a4d8f0bc017aea1765075fdc500be8074b3c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 16 Apr 2020 00:55:04 +0900 Subject: [PATCH] update mathcomp packages --- .../coq-mathcomp-algebra.1.11.0+beta1/opam | 27 +++++++++++++++++ .../coq-mathcomp-character.1.11.0+beta1/opam | 25 ++++++++++++++++ .../coq-mathcomp-field.1.11.0+beta1/opam | 25 ++++++++++++++++ .../coq-mathcomp-fingroup.1.11.0+beta1/opam | 25 ++++++++++++++++ .../coq-mathcomp-solvable.1.11.0+beta1/opam | 25 ++++++++++++++++ .../coq-mathcomp-ssreflect.1.11.0+beta1/opam | 29 +++++++++++++++++++ 6 files changed, 156 insertions(+) create mode 100644 released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.11.0+beta1/opam create mode 100644 released/packages/coq-mathcomp-character/coq-mathcomp-character.1.11.0+beta1/opam create mode 100644 released/packages/coq-mathcomp-field/coq-mathcomp-field.1.11.0+beta1/opam create mode 100644 released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.11.0+beta1/opam create mode 100644 released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.11.0+beta1/opam create mode 100644 released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.11.0+beta1/opam diff --git a/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.11.0+beta1/opam b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.11.0+beta1/opam new file mode 100644 index 0000000000..a09212a902 --- /dev/null +++ b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.11.0+beta1/opam @@ -0,0 +1,27 @@ +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:algebra" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.algebra" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +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: "http://github.com/math-comp/math-comp/archive/mathcomp-1.11.0+beta1.tar.gz" +checksum: "sha256=0f71bb8b512416881984e18b922d2bae78bc00819492f4ab28348d2d9488a517" +} diff --git a/released/packages/coq-mathcomp-character/coq-mathcomp-character.1.11.0+beta1/opam b/released/packages/coq-mathcomp-character/coq-mathcomp-character.1.11.0+beta1/opam new file mode 100644 index 0000000000..07597c6fc6 --- /dev/null +++ b/released/packages/coq-mathcomp-character/coq-mathcomp-character.1.11.0+beta1/opam @@ -0,0 +1,25 @@ +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:algebra" "keyword:character" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.character" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on character theory" +description:""" +This library contains definitions and theorems about group +representations, characters and class functions. +""" + +url { +src: "http://github.com/math-comp/math-comp/archive/mathcomp-1.11.0+beta1.tar.gz" +checksum: "sha256=0f71bb8b512416881984e18b922d2bae78bc00819492f4ab28348d2d9488a517" +} diff --git a/released/packages/coq-mathcomp-field/coq-mathcomp-field.1.11.0+beta1/opam b/released/packages/coq-mathcomp-field/coq-mathcomp-field.1.11.0+beta1/opam new file mode 100644 index 0000000000..b68c86660e --- /dev/null +++ b/released/packages/coq-mathcomp-field/coq-mathcomp-field.1.11.0+beta1/opam @@ -0,0 +1,25 @@ +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:algebra" "keyword:field" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.field" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on Fields" +description:""" +This library contains definitions and theorems about field extensions, +galois theory, algebraic numbers, cyclotomic polynomials... +""" + +url { +src: "http://github.com/math-comp/math-comp/archive/mathcomp-1.11.0+beta1.tar.gz" +checksum: "sha256=0f71bb8b512416881984e18b922d2bae78bc00819492f4ab28348d2d9488a517" +} diff --git a/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.11.0+beta1/opam b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.11.0+beta1/opam new file mode 100644 index 0000000000..682f7c0c5d --- /dev/null +++ b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.11.0+beta1/opam @@ -0,0 +1,25 @@ +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:finite groups" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.fingroup" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +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: "http://github.com/math-comp/math-comp/archive/mathcomp-1.11.0+beta1.tar.gz" +checksum: "sha256=0f71bb8b512416881984e18b922d2bae78bc00819492f4ab28348d2d9488a517" +} diff --git a/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.11.0+beta1/opam b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.11.0+beta1/opam new file mode 100644 index 0000000000..2bdf476d92 --- /dev/null +++ b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.11.0+beta1/opam @@ -0,0 +1,25 @@ +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:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.solvable" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +synopsis: "Mathematical Components Library on finite groups (II)" + +description:""" +This library contains more definitions and theorems about finite groups. +""" + +url { +src: "http://github.com/math-comp/math-comp/archive/mathcomp-1.11.0+beta1.tar.gz" +checksum: "sha256=0f71bb8b512416881984e18b922d2bae78bc00819492f4ab28348d2d9488a517" +} diff --git a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.11.0+beta1/opam b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.11.0+beta1/opam new file mode 100644 index 0000000000..c7520477ff --- /dev/null +++ b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.11.0+beta1/opam @@ -0,0 +1,29 @@ +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.7" & < "8.12~") | (= "dev"))} ] + +tags: [ "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.ssreflect" ] +authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] + +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: "http://github.com/math-comp/math-comp/archive/mathcomp-1.11.0+beta1.tar.gz" +checksum: "sha256=0f71bb8b512416881984e18b922d2bae78bc00819492f4ab28348d2d9488a517" +}