From 2ff904321928451e59efb44948b8bbda9f2c9d56 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 25 Oct 2024 19:31:26 +0900 Subject: [PATCH 1/2] release MathComp-Analysis 1.6.0 --- .../coq-mathcomp-analysis.1.6.0/opam | 67 +++++++++++++++++++ .../coq-mathcomp-classical.1.6.0/opam | 53 +++++++++++++++ 2 files changed, 120 insertions(+) create mode 100644 released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.1.6.0/opam create mode 100644 released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam diff --git a/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.1.6.0/opam b/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.1.6.0/opam new file mode 100644 index 000000000..f82398773 --- /dev/null +++ b/released/packages/coq-mathcomp-analysis/coq-mathcomp-analysis.1.6.0/opam @@ -0,0 +1,67 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "An analysis library for mathematical components" +description: """ +This repository contains an experimental library for real analysis for +the Coq proof-assistant and using the Mathematical Components library.""" + +build: [make "-C" "theories" "-j%{jobs}%"] +install: [make "-C" "theories" "install"] +depends: [ + "coq" { (>= "8.19" & < "8.21~") | (= "dev") } + "coq-mathcomp-classical" { = version} + "coq-mathcomp-solvable" { (>= "2.0.0") } + "coq-mathcomp-field" + "coq-mathcomp-bigenough" { (>= "1.0.0") } +] + +tags: [ + "category:Mathematics/Real Calculus and Topology" + "keyword:analysis" + "keyword:extended real numbers" + "keyword:filter" + "keyword:Cantor" + "keyword:topology" + "keyword:real numbers" + "keyword:sequence" + "keyword:convexity" + "keyword:Landau notation" + "keyword:logarithm" + "keyword:sin" + "keyword:cos" + "keyword:tangent" + "keyword:trigonometric function" + "keyword:exponential" + "keyword:differentiation" + "keyword:derivative" + "keyword:measure theory" + "keyword:integration" + "keyword:Lebesgue" + "keyword:probability" + "logpath:mathcomp.analysis" + "date:2024-10-25" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] +url { + src: "https://github.com/math-comp/analysis/releases/download/1.6.0/analysis-1.6.0.tar.gz" + checksum: "sha512=c65a3386459fb31279b19b77b6b1a8794811c84b9253949a9a49f55cc6e57925412261a80fddd88f99814078b2dc174b35772783e3ddb301f53a4df345213615" +} diff --git a/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam b/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam new file mode 100644 index 000000000..92c959b33 --- /dev/null +++ b/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam @@ -0,0 +1,53 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " + +homepage: "https://github.com/math-comp/analysis" +dev-repo: "git+https://github.com/math-comp/analysis.git" +bug-reports: "https://github.com/math-comp/analysis/issues" +license: "CECILL-C" + +synopsis: "A library for classical logic for mathematical components" +description: """ +This repository contains a library for classical logic for +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" & < "8.21~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.1.0") } + "coq-mathcomp-fingroup" + "coq-mathcomp-algebra" + "coq-mathcomp-finmap" { (>= "2.0.0") | (= "dev") } + "coq-hierarchy-builder" { (>= "1.4.0") } +] + +tags: [ + "category:Mathematics/Classical Logic" + "keyword:classical" + "keyword:logic" + "keyword:sets" + "keyword:set theory" + "keyword:function" + "keyword:cardinal" + "logpath:mathcomp.classical" + "date:2024-10-25" +] +authors: [ + "Reynald Affeldt" + "Alessandro Bruni" + "Yves Bertot" + "Cyril Cohen" + "Marie Kerjean" + "Assia Mahboubi" + "Damien Rouhling" + "Pierre Roux" + "Kazuhiko Sakaguchi" + "Zachary Stone" + "Pierre-Yves Strub" + "Laurent Théry" +] +url { + src: "https://github.com/math-comp/analysis/releases/download/1.6.0/analysis-1.6.0.tar.gz" + checksum: "sha512=c65a3386459fb31279b19b77b6b1a8794811c84b9253949a9a49f55cc6e57925412261a80fddd88f99814078b2dc174b35772783e3ddb301f53a4df345213615" +} From 153ac97ff268df2668038daef3f4d9e692c420f5 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 25 Oct 2024 21:49:18 +0900 Subject: [PATCH 2/2] Update released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam Co-authored-by: Karl Palmskog --- .../coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam b/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam index 92c959b33..a97c868c2 100644 --- a/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam +++ b/released/packages/coq-mathcomp-classical/coq-mathcomp-classical.1.6.0/opam @@ -18,7 +18,7 @@ depends: [ "coq-mathcomp-ssreflect" { (>= "2.1.0") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" - "coq-mathcomp-finmap" { (>= "2.0.0") | (= "dev") } + "coq-mathcomp-finmap" { (>= "2.0.0") } "coq-hierarchy-builder" { (>= "1.4.0") } ]