Merge pull request #3264 from affeldt-aist/infotheo.0.7.6

release infotheo 0.7.6
coq · Dec 19, 2024 · 60aef35 · 60aef35
2 parents 1962dec + 18bccca
commit 60aef35
Show file tree

Hide file tree

Showing 2 changed files with 60 additions and 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
@@ -18,11 +18,11 @@ build: [
 install: [make "install"]
 depends: [
   "coq" { (>= "8.19" & < "8.21~") | (= "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-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" }

diff --git a/released/packages/coq-infotheo/coq-infotheo.0.7.6/opam b/released/packages/coq-infotheo/coq-infotheo.0.7.6/opam
@@ -0,0 +1,55 @@
+opam-version: "2.0"
+maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
+
+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.3.0") }
+  "coq-mathcomp-fingroup" { (>= "2.3.0") }
+  "coq-mathcomp-algebra" { (>= "2.3.0") }
+  "coq-mathcomp-solvable" { (>= "2.3.0") }
+  "coq-mathcomp-field" { (>= "2.3.0") }
+  "coq-mathcomp-analysis" { (>= "1.7.0") }
+  "coq-mathcomp-reals-stdlib" { (>= "1.7.0") }
+  "coq-hierarchy-builder" { (>= "1.5.0" & < "1.8.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-12-19"
+]
+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.6.tar.gz"
+  checksum: "sha512=60811b68caba4e575fc93afa4db7a191c17eb378b90972d10e8fb97d29be2a4ccf2f25eece1af2fb325636cc68597962040aea5818f56c6b610307daf2bccc3e"
+}