From 6cd71a13a56a88072eadcd16482b67a6b692fb85 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 Nov 2024 16:57:48 +0900 Subject: [PATCH 1/3] release infotheo 0.7.5 --- .../coq-infotheo/coq-infotheo.0.7.5/opam | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 released/packages/coq-infotheo/coq-infotheo.0.7.5/opam diff --git a/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam b/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam new file mode 100644 index 0000000000..0fe1915fad --- /dev/null +++ b/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam @@ -0,0 +1,55 @@ +opam-version: "2.0" +maintainer: "Reynald Affeldt " + +homepage: "https://github.com/affeldt-aist/infotheo" +dev-repo: "git+https://github.com/affeldt-aist/infotheo.git" +bug-reports: "https://github.com/affeldt-aist/infotheo/issues" +license: "LGPL-2.1-or-later" + +synopsis: "Discrete probabilities and information theory for Coq" +description: """ +Infotheo is a Coq library for reasoning about discrete probabilities, +information theory, and linear error-correcting codes.""" + +build: [ + [make "-j%{jobs}%" ] + [make "-C" "extraction" "tests"] {with-test} +] +install: [make "install"] +depends: [ + "coq" { (>= "8.19" & < "8.21~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-analysis" { (>= "1.7.0") } + "coq-mathcomp-reals-stdlib" { (>= "1.7.0) } + "coq-hierarchy-builder" { >= "1.5.0" } + "coq-mathcomp-algebra-tactics" { >= "1.2.0" } + "coq-interval" { >= "4.10.0"} +] + +tags: [ + "keyword:information theory" + "keyword:probability" + "keyword:error-correcting codes" + "keyword:convexity" + "logpath:infotheo" + "date:2024-11-29" +] +authors: [ + "Reynald Affeldt, AIST" + "Manabu Hagiwara, Chiba U. (previously AIST)" + "Jonas Senizergues, ENS Cachan (internship at AIST)" + "Jacques Garrigue, Nagoya U." + "Kazuhiko Sakaguchi, Tsukuba U." + "Taku Asai, Nagoya U. (M2)" + "Takafumi Saikawa, Nagoya U." + "Naruomi Obata, Titech (M2)" + "Alessandro Bruni, IT-University of Copenhagen" +] +url { + src: "https://github.com/affeldt-aist/infotheo/archive/0.7.5.tar.gz" + checksum: "sha512=f1f357bf5b4eb455401f05ac7bfc235998b6d91ae9aa6ef4d92ee77a9ab592bc5e6dc9a6f603435e5e2d4ee5219225f3502acb1172ab68ca824d282c90ba5fd5" +} From 0a9f1a1f7027d5a0345b918d78c77509fcb6e7d3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 29 Nov 2024 17:09:55 +0900 Subject: [PATCH 2/3] fix --- released/packages/coq-infotheo/coq-infotheo.0.7.5/opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam b/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam index 0fe1915fad..3527450111 100644 --- a/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam +++ b/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam @@ -24,7 +24,7 @@ depends: [ "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") } "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") } "coq-mathcomp-analysis" { (>= "1.7.0") } - "coq-mathcomp-reals-stdlib" { (>= "1.7.0) } + "coq-mathcomp-reals-stdlib" { (>= "1.7.0") } "coq-hierarchy-builder" { >= "1.5.0" } "coq-mathcomp-algebra-tactics" { >= "1.2.0" } "coq-interval" { >= "4.10.0"} From 44321c40a9dc97d06218b5a2910154d662f6dc68 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 29 Nov 2024 17:20:56 +0900 Subject: [PATCH 3/3] Update released/packages/coq-infotheo/coq-infotheo.0.7.5/opam Co-authored-by: Karl Palmskog --- released/packages/coq-infotheo/coq-infotheo.0.7.5/opam | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam b/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam index 3527450111..983d9598cc 100644 --- a/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam +++ b/released/packages/coq-infotheo/coq-infotheo.0.7.5/opam @@ -18,11 +18,11 @@ build: [ install: [make "install"] depends: [ "coq" { (>= "8.19" & < "8.21~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") } - "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.2.0") } + "coq-mathcomp-fingroup" { (>= "2.2.0") } + "coq-mathcomp-algebra" { (>= "2.2.0") } + "coq-mathcomp-solvable" { (>= "2.2.0") } + "coq-mathcomp-field" { (>= "2.2.0") } "coq-mathcomp-analysis" { (>= "1.7.0") } "coq-mathcomp-reals-stdlib" { (>= "1.7.0") } "coq-hierarchy-builder" { >= "1.5.0" }