coq-infotheo.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
version: "dev"

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") }
  "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" }
  "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"
]
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"
]