From b05778d64c6cf39400e1af26abf3eb528951441e Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 28 Sep 2023 15:45:32 +0200 Subject: [PATCH] Release coq-mathcomp-algebra-tactics.1.2.0 --- .../coq-mathcomp-algebra-tactics.dev/opam | 25 +++++++---- .../coq-mathcomp-algebra-tactics.1.2.0/opam | 45 +++++++++++++++++++ 2 files changed, 61 insertions(+), 9 deletions(-) create mode 100644 released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.0/opam diff --git a/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam b/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam index 120995322..f6a8295c7 100644 --- a/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam +++ b/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam @@ -6,17 +6,23 @@ dev-repo: "git+https://github.com/math-comp/algebra-tactics.git" bug-reports: "https://github.com/math-comp/algebra-tactics/issues" license: "CECILL-B" -synopsis: "Ring and field tactics for Mathematical Components" +synopsis: "Ring, field, lra, nra, and psatz tactics for Mathematical Components" description: """ -This library provides `ring` and `field` tactics for Mathematical Components, -that work with any `comRingType` and `fieldType` instances, respectively. -Their instance resolution is done through canonical structure inference. -Therefore, they work with abstract rings and do not require `Add Ring` and -`Add Field` commands. Another key feature of this library is that they -automatically push down ring morphisms and additive functions to leaves of -ring/field expressions before normalization to the Horner form.""" +This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for +algebraic structures of the Mathematical Components library. The `ring` tactic +works with any `comRingType` (commutative ring) or `comSemiRingType` +(commutative semiring). The `field` tactic works with any `fieldType` (field). +The other (Micromega) tactics work with any `realDomainType` (totally ordered +integral domain) or `realFieldType` (totally ordered field). Algebra Tactics +do not provide a way to declare instances, like the `Add Ring` and `Add Field` +commands, but use canonical structure inference instead. Therefore, each of +these tactics works with any canonical (or abstract) instance of the +respective structure declared through Hierarchy Builder. Another key feature +of Algebra Tactics is that they automatically push down ring morphisms and +additive functions to leaves of ring/field expressions before applying the +proof procedures.""" -build: [make "-j%{jobs}%" ] +build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "coq" {>= "8.16"} @@ -31,6 +37,7 @@ tags: [ ] authors: [ "Kazuhiko Sakaguchi" + "Pierre Roux" ] url { src: "git+https://github.com/math-comp/algebra-tactics.git#master" diff --git a/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.0/opam b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.0/opam new file mode 100644 index 000000000..84cef1deb --- /dev/null +++ b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.0/opam @@ -0,0 +1,45 @@ +opam-version: "2.0" +maintainer: "kazuhiko.sakaguchi@inria.fr" + +homepage: "https://github.com/math-comp/algebra-tactics" +dev-repo: "git+https://github.com/math-comp/algebra-tactics.git" +bug-reports: "https://github.com/math-comp/algebra-tactics/issues" +license: "CECILL-B" + +synopsis: "Ring, field, lra, nra, and psatz tactics for Mathematical Components" +description: """ +This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for +algebraic structures of the Mathematical Components library. The `ring` tactic +works with any `comRingType` (commutative ring) or `comSemiRingType` +(commutative semiring). The `field` tactic works with any `fieldType` (field). +The other (Micromega) tactics work with any `realDomainType` (totally ordered +integral domain) or `realFieldType` (totally ordered field). Algebra Tactics +do not provide a way to declare instances, like the `Add Ring` and `Add Field` +commands, but use canonical structure inference instead. Therefore, each of +these tactics works with any canonical (or abstract) instance of the +respective structure declared through Hierarchy Builder. Another key feature +of Algebra Tactics is that they automatically push down ring morphisms and +additive functions to leaves of ring/field expressions before applying the +proof procedures.""" + +build: [make "-j%{jobs}%"] +install: [make "install"] +depends: [ + "coq" {>= "8.16" & < "8.19~"} + "coq-mathcomp-ssreflect" {>= "2.0" & < "2.1~"} + "coq-mathcomp-algebra" + "coq-mathcomp-zify" {>= "1.5.0"} + "coq-elpi" {>= "1.15.0" & != "1.17.0"} +] + +tags: [ + "logpath:mathcomp.algebra_tactics" +] +authors: [ + "Kazuhiko Sakaguchi" + "Pierre Roux" +] +url { + src: "https://github.com/math-comp/algebra-tactics/archive/refs/tags/1.2.0.tar.gz" + checksum: "sha256=c3b1275cb5662fe70b131a912979b19dbffde80ac28d97ca06a243737741dcb1" +}