From 7db87cdd188547bcde461dc3f5086bf2a77ab2af Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 27 Aug 2026 14:58:54 +0200 Subject: [PATCH] Add rocq-mathcomp-zify dev and 1.7.0+2.4+9.0 --- .../coq-mathcomp-zify.dev/opam | 25 ++------------ .../rocq-mathcomp-zify.dev/opam | 32 ++++++++++++++++++ .../coq-mathcomp-zify.1.7.0+2.4+9.0/opam | 12 +++++++ .../rocq-mathcomp-zify.1.7.0+2.4+9.0/opam | 33 +++++++++++++++++++ 4 files changed, 80 insertions(+), 22 deletions(-) create mode 100644 extra-dev/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.dev/opam create mode 100644 released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.7.0+2.4+9.0/opam create mode 100644 released/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.1.7.0+2.4+9.0/opam diff --git a/extra-dev/packages/coq-mathcomp-zify/coq-mathcomp-zify.dev/opam b/extra-dev/packages/coq-mathcomp-zify/coq-mathcomp-zify.dev/opam index 4a698f29da..ef120f97e8 100644 --- a/extra-dev/packages/coq-mathcomp-zify/coq-mathcomp-zify.dev/opam +++ b/extra-dev/packages/coq-mathcomp-zify/coq-mathcomp-zify.dev/opam @@ -6,26 +6,7 @@ dev-repo: "git+https://github.com/math-comp/mczify.git" bug-reports: "https://github.com/math-comp/mczify/issues" license: "CECILL-B" -synopsis: "Micromega tactics for Mathematical Components" -description: """ -This small library enables the use of the Micromega tactics for goals stated -with the definitions of the Mathematical Components library by extending the -zify tactic.""" +depends: [ "rocq-mathcomp-zify" { = version } ] +authors: [ "Kazuhiko Sakaguchi" ] -build: [make "-j%{jobs}%" ] -install: [make "install"] -depends: [ - "coq" {>= "8.16"} - "coq-mathcomp-ssreflect" {>= "2.0"} - "coq-mathcomp-algebra" -] - -tags: [ - "logpath:mathcomp.zify" -] -authors: [ - "Kazuhiko Sakaguchi" -] -url { - src: "git+https://github.com/math-comp/mczify.git#master" -} +synopsis: "Compatibility package for rocq-mathcomp-zify" diff --git a/extra-dev/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.dev/opam b/extra-dev/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.dev/opam new file mode 100644 index 0000000000..8ebf352d65 --- /dev/null +++ b/extra-dev/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.dev/opam @@ -0,0 +1,32 @@ +opam-version: "2.0" +maintainer: "kazuhiko.sakaguchi@inria.fr" + +homepage: "https://github.com/math-comp/mczify" +dev-repo: "git+https://github.com/math-comp/mczify.git" +bug-reports: "https://github.com/math-comp/mczify/issues" +license: "CECILL-B" + +synopsis: "Micromega tactics for Mathematical Components" +description: """ +This small library enables the use of the Micromega arithmetic solvers of Rocq +for goals stated with the definitions of the Mathematical Components library +by extending the zify tactic.""" + +build: [make "-j%{jobs}%" ] +install: [make "install"] +depends: [ + "rocq-core" {>= "9.0"} + "rocq-stdlib" + "rocq-mathcomp-ssreflect" {>= "2.4"} + "rocq-mathcomp-algebra" +] + +tags: [ + "logpath:mathcomp.zify" +] +authors: [ + "Kazuhiko Sakaguchi" +] +url { + src: "git+https://github.com/math-comp/mczify.git#master" +} diff --git a/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.7.0+2.4+9.0/opam b/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.7.0+2.4+9.0/opam new file mode 100644 index 0000000000..ef120f97e8 --- /dev/null +++ b/released/packages/coq-mathcomp-zify/coq-mathcomp-zify.1.7.0+2.4+9.0/opam @@ -0,0 +1,12 @@ +opam-version: "2.0" +maintainer: "kazuhiko.sakaguchi@inria.fr" + +homepage: "https://github.com/math-comp/mczify" +dev-repo: "git+https://github.com/math-comp/mczify.git" +bug-reports: "https://github.com/math-comp/mczify/issues" +license: "CECILL-B" + +depends: [ "rocq-mathcomp-zify" { = version } ] +authors: [ "Kazuhiko Sakaguchi" ] + +synopsis: "Compatibility package for rocq-mathcomp-zify" diff --git a/released/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.1.7.0+2.4+9.0/opam b/released/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.1.7.0+2.4+9.0/opam new file mode 100644 index 0000000000..30db1febb7 --- /dev/null +++ b/released/packages/rocq-mathcomp-zify/rocq-mathcomp-zify.1.7.0+2.4+9.0/opam @@ -0,0 +1,33 @@ +opam-version: "2.0" +maintainer: "kazuhiko.sakaguchi@inria.fr" + +homepage: "https://github.com/math-comp/mczify" +dev-repo: "git+https://github.com/math-comp/mczify.git" +bug-reports: "https://github.com/math-comp/mczify/issues" +license: "CECILL-B" + +synopsis: "Micromega tactics for Mathematical Components" +description: """ +This small library enables the use of the Micromega arithmetic solvers of Rocq +for goals stated with the definitions of the Mathematical Components library +by extending the zify tactic.""" + +build: [make "-j%{jobs}%"] +install: [make "install"] +depends: [ + "rocq-core" {>= "9.0" & < "9.4~"} + "rocq-stdlib" + "rocq-mathcomp-ssreflect" {>= "2.4" & < "2.7~"} + "rocq-mathcomp-algebra" +] + +tags: [ + "logpath:mathcomp.zify" +] +authors: [ + "Kazuhiko Sakaguchi" +] +url { + src: "https://github.com/math-comp/mczify/archive/refs/tags/1.7.0+2.4+9.0.tar.gz" + checksum: "sha256=649fa3d82be1cc606261e25b6fd26ddc5b55b2e6697a314b20f0564273089a54" +}