From 65cdc490b3ed5a4fc7d1f2f7a5445b106589be76 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 14 Dec 2020 17:19:47 +0900 Subject: [PATCH] use coq-templates to generate utility files --- .github/workflows/docker-action.yml | 32 ++++++ LICENSE.txt => LICENSE | 0 README.md | 121 ++++++++++++++++++++ README.org | 74 ------------ changelog.txt | 15 ++- coq-infotheo.opam | 48 ++++++++ dune | 7 ++ dune-project | 6 + index.md | 59 ++++++++++ infotheo_authors.txt | 25 ---- meta.yml | 170 ++++++++++++++++++++++++++++ opam | 44 ------- 12 files changed, 454 insertions(+), 147 deletions(-) create mode 100644 .github/workflows/docker-action.yml rename LICENSE.txt => LICENSE (100%) create mode 100644 README.md delete mode 100644 README.org create mode 100644 coq-infotheo.opam create mode 100644 dune create mode 100644 dune-project create mode 100644 index.md delete mode 100644 infotheo_authors.txt create mode 100644 meta.yml delete mode 100644 opam diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 00000000..4d71fc74 --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -0,0 +1,32 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Docker CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'mathcomp/mathcomp:1.11.0-coq-8.11' + - 'mathcomp/mathcomp:1.11.0-coq-8.12' + fail-fast: false + steps: + - uses: actions/checkout@v2 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-infotheo.opam' + custom_image: ${{ matrix.image }} + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/LICENSE.txt b/LICENSE similarity index 100% rename from LICENSE.txt rename to LICENSE diff --git a/README.md b/README.md new file mode 100644 index 00000000..7415d81a --- /dev/null +++ b/README.md @@ -0,0 +1,121 @@ + +# A Coq formalization of information theory and linear error correcting codes + +[![Docker CI][docker-action-shield]][docker-action-link] + +[docker-action-shield]: https://github.com/affeldt-aist/infotheo/workflows/Docker%20CI/badge.svg?branch=master +[docker-action-link]: https://github.com/affeldt-aist/infotheo/actions?query=workflow:"Docker%20CI" + + + + +Infotheo is a Coq library for reasoning about discrete probabilities, +information theory, and linear error-correcting codes. + +## Meta + +- Author(s): + - Reynald Affeldt, AIST (initial) + - Manabu Hagiwara, Chiba U. (previously AIST) (initial) + - Jonas Senizergues, ENS Cachan (internship at AIST) (initial) + - Jacques Garrigue, Nagoya U. + - Kazuhiko Sakaguchi, Tsukuba U. + - Taku Asai, Nagoya U. (M2) + - Takafumi Saikawa, Nagoya U. + - Naruomi Obata, Titech (M2) +- License: [LGPL-2.1-or-later](LICENSE) +- Compatible Coq versions: Coq 8.11 to 8.12 +- Additional dependencies: + - [MathComp ssreflect 1.11](https://math-comp.github.io) + - [MathComp fingroup 1.11](https://math-comp.github.io) + - [MathComp algebra 1.11](https://math-comp.github.io) + - [MathComp solvable 1.11](https://math-comp.github.io) + - [MathComp field 1.11](https://math-comp.github.io) + - [MathComp analysis 0.3.4](https://github.com/math-comp/analysis) +- Coq namespace: `infotheo` +- Related publication(s): + - [Formal Adventures in Convex and Conical Spaces](https://arxiv.org/abs/2004.12713) doi:[10.1007/978-3-030-53518-6_2](https://doi.org/10.1007/978-3-030-53518-6_2) + - [A Library for Formalization of Linear Error-Correcting Codes](https://link.springer.com/article/10.1007/s10817-019-09538-8) doi:[10.1007/s10817-019-09538-8](https://doi.org/10.1007/s10817-019-09538-8) + - [Reasoning with Conditional Probabilities and Joint Distributions in Coq](https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en) doi:[10.11309/jssst.37.3_79](https://doi.org/10.11309/jssst.37.3_79) + - [Examples of formal proofs about data compression](http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf) doi:[10.23919/ISITA.2018.8664276](https://doi.org/10.23919/ISITA.2018.8664276) + - [Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes](http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf) + - [Formalization of error-correcting codes---from Hamming to modern coding theory](http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf) doi:[10.1007/978-3-319-22102-1_2](https://doi.org/10.1007/978-3-319-22102-1_2) + - [Formalization of Shannon’s Theorems](https://link.springer.com/article/10.1007%2Fs10817-013-9298-1) doi:[10.1007/s10817-013-9298-1](https://doi.org/10.1007/s10817-013-9298-1) + +## Building and installation instructions + +The easiest way to install the latest released version of A Coq formalization of information theory and linear error correcting codes +is via [OPAM](https://opam.ocaml.org/doc/Install.html): + +```shell +opam repo add coq-released https://coq.inria.fr/opam/released +opam install coq-infotheo +``` + +To instead build and install manually, do: + +``` shell +git clone https://github.com/affeldt-aist/infotheo.git +cd infotheo +make # or make -j +make install +``` + + +## Acknowledgments + +Many thanks to [various contributors](https://github.com/affeldt-aist/infotheo/graphs/contributors) + +The principle of inclusion-exclusion is a contribution by +Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory) +(main theorem: Pr_bigcup_incl_excl; commit 956096859ed89325b2bb74033690ac882bbcd64e) + +The variable-length source coding theorems are a contribution by +Ryosuke Obi (Chiba U. (M2)) +(commit a67da5e24eaaabb345d225a5bd0f5e86d35413a8) +(with Manabu Hagiwara and Mitsuharu Yamamoto) + +Commit 64814f529c1819684c4b8060d0779c24c6339041 was originally by Karl Palmskog + +The formalization of modern coding theory is a collaboration with +K. Kasai, S. Kuzuoka, R. Obi + +Y. Takahashi collaborated to the formalization of linear error-correcting codes + +This work was partially supported by a JSPS Grant-in-Aid for Scientific +Research (Project Number: 25289118), a JSPS Grand-in-Aid for Scientific Research (Project Number: 18H03204) + +## Documentation + +Each file is documented in its header. + +Changes are documented in [changelog.txt](changelog.txt). + +## Installation with Windows 10 (TODO: update) + +Installation of infotheo on Windows is less simple. +See [this page](https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org) +for instructions to install MathComp on Windows 10 +(or [this page](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html) for instructions in Japanese). +Once MathComp is installed, two options: + +1. You have installed MathComp with opam. + Then do: + `opam install coq-infotheo` or `git clone git@github.com:affeldt-aist/infotheo.git; opam install .` + +2. You have installed MathComp using unzip, untar, cd, make, make install. + Then do: + - Install MathComp-Analysis using unzip, untar, cd, make, make install + + Install bigenough 1.0.0 [download](https://github.com/math-comp/bigenough) + + Install finmap 1.5.0 [download](https://github.com/math-comp/finmap) + + Install analysis 0.3.2 [download](https://github.com/math-comp/analysis) + - Install infotheo using `coq_makefile`, `make`, `make install` as explained above + [download](https://github.com/affeldt-aist/infotheo) + +## Original License + +Before version 0.2, infotheo was distributed under the terms of the +`GPL-3.0-or-later` license. diff --git a/README.org b/README.org deleted file mode 100644 index e6241a95..00000000 --- a/README.org +++ /dev/null @@ -1,74 +0,0 @@ -* infotheo - -[[https://travis-ci.com/affeldt-aist/infotheo][file:https://travis-ci.com/affeldt-aist/infotheo.svg?branch=master]] - -** Installation - - The preferred way to install infotheo is with opam because it takes - care of the dependencies with other libraries. If not already done, - add the repository for Coq libraries to opam and update: - -1. ~opam repo add coq-released https://coq.inria.fr/opam/released~ -2. ~opam update~ - -*** Last stable version: - -Version 0.2: -3. ~opam install coq-infotheo~ - -**** Requirements - -- [[https://coq.inria.fr][Coq]] 8.11 or 8.12 -- [[https://github.com/math-comp/math-comp][Mathematical Components library]] 1.11.0 -- [[https://github.com/math-comp/analysis][MathComp-Analysis]] 0.3.2 - which requires - + [[https://github.com/math-comp/finmap][finmap]] 1.5.0 or greater - -All versions available from opam. - -*** Development version (git master): - -1. ~git clone git@github.com:affeldt-aist/infotheo.git~ -2. ~cd infotheo~ - -If opam is installed, do: - -3. ~opam install .~ - -If opam is not installed but if the requirements are met, do: - -3. ~make~ -4. ~make install~ - -*** About Windows 10 - -Installation of infotheo on Windows is less simple. -See [[https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org][this page]] for instructions to install MathComp on Windows 10 -(or [[https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html][this page]] for instructions in Japanese). -Once MathComp is installed, two options: -1. You have installed MathComp with opam. - Then do: - + ~opam install coq-infotheo~ or ~git clone git@github.com:affeldt-aist/infotheo.git; opam install .~ -2. You have installed MathComp using unzip, untar, cd, make, make install. - Then do: - + Install MathComp-Analysis using unzip, untar, cd, make, make install - 1. Install bigenough 1.0.0 ([[https://github.com/math-comp/bigenough][download]]) - 2. Install finmap 1.5.0 ([[https://github.com/math-comp/finmap][download]]) - 3. Install analysis 0.3.2 ([[https://github.com/math-comp/analysis][download]]) - + Install infotheo using ~coq_makefile~, ~make~, ~make install~ as explained above ([[https://github.com/affeldt-aist/infotheo][download]]) - -** License - -LGPL-2.1-or-later - -(Before version 0.2, infotheo was distributed under the terms of the -~GPL-3.0-or-later~ license.) - -** Authors - -See [[infotheo_authors.txt]] - -** References - -There are a few papers available [[https://staff.aist.go.jp/reynald.affeldt/shannon/][here]] that provide explanations and references. - diff --git a/changelog.txt b/changelog.txt index d1288dd8..f986a31f 100644 --- a/changelog.txt +++ b/changelog.txt @@ -3,11 +3,18 @@ from 0.2 to 0.? --------------- - changed: - + in ssrZ.v: - * Z_of_nat_le -> leZ_nat, Z_of_nat_lt -> ltZ_nat - * Z<=nat -> %:Z + + in ssrZ.v: + * Z_of_nat_le -> leZ_nat, Z_of_nat_lt -> ltZ_nat + * Z<=nat -> %:Z - removed: - + in classical_sets_ext: set1_inj + + in classical_sets_ext: + set1_inj +- renamed: + + in classical_sets_ext.v: + image_subset -> subset_image +- remove: + + in classical_sets_ext.v: + fullimage_subset ----------------- from 0.1.2 to 0.2 diff --git a/coq-infotheo.opam b/coq-infotheo.opam new file mode 100644 index 00000000..11b87f04 --- /dev/null +++ b/coq-infotheo.opam @@ -0,0 +1,48 @@ +# 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 " +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.11" & < "8.13~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-fingroup" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-algebra" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-solvable" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-field" { (>= "1.11.0" & < "1.12~") } + "coq-mathcomp-analysis" { (= "0.3.4") } +] + +tags: [ + "keyword:information theory" + "keyword:probability" + "keyword:error-correcting codes" + "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)" +] diff --git a/dune b/dune new file mode 100644 index 00000000..13f7a06a --- /dev/null +++ b/dune @@ -0,0 +1,7 @@ +; This file was generated from `meta.yml`, please do not edit manually. +; Follow the instructions on https://github.com/coq-community/templates to regenerate. + +(coq.theory + (name infotheo) + (package coq-infotheo) + (synopsis "Discrete probabilities and information theory for Coq")) diff --git a/dune-project b/dune-project new file mode 100644 index 00000000..f60d9a67 --- /dev/null +++ b/dune-project @@ -0,0 +1,6 @@ +; This file was generated from `meta.yml`, please do not edit manually. +; Follow the instructions on https://github.com/coq-community/templates to regenerate. + +(lang dune 2.5) +(using coq 0.2) +(name infotheo) diff --git a/index.md b/index.md new file mode 100644 index 00000000..f03a76bc --- /dev/null +++ b/index.md @@ -0,0 +1,59 @@ +--- +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +title: A Coq formalization of information theory and linear error correcting codes +lang: en +header-includes: + - | + + + + + +--- + +
+View the project on GitHub +
+ +## About + +Welcome to the A Coq formalization of information theory and linear error correcting codes project website! + +Infotheo is a Coq library for reasoning about discrete probabilities, +information theory, and linear error-correcting codes. + +This is an open source project, licensed under the LGPL-2.1-or-later. + +## Get the code + +The current stable release of A Coq formalization of information theory and linear error correcting codes can be [downloaded from GitHub](https://github.com/affeldt-aist/infotheo/releases). + +## Documentation + + +Related publications, if any, are listed below. + +- [Formal Adventures in Convex and Conical Spaces](https://arxiv.org/abs/2004.12713) doi:[10.1007/978-3-030-53518-6_2](https://doi.org/10.1007/978-3-030-53518-6_2) +- [A Library for Formalization of Linear Error-Correcting Codes](https://link.springer.com/article/10.1007/s10817-019-09538-8) doi:[10.1007/s10817-019-09538-8](https://doi.org/10.1007/s10817-019-09538-8) +- [Reasoning with Conditional Probabilities and Joint Distributions in Coq](https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en) doi:[10.11309/jssst.37.3_79](https://doi.org/10.11309/jssst.37.3_79) +- [Examples of formal proofs about data compression](http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf) doi:[10.23919/ISITA.2018.8664276](https://doi.org/10.23919/ISITA.2018.8664276) +- [Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes](http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf) +- [Formalization of error-correcting codes---from Hamming to modern coding theory](http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf) doi:[10.1007/978-3-319-22102-1_2](https://doi.org/10.1007/978-3-319-22102-1_2) +- [Formalization of Shannon’s Theorems](https://link.springer.com/article/10.1007%2Fs10817-013-9298-1) doi:[10.1007/s10817-013-9298-1](https://doi.org/10.1007/s10817-013-9298-1) + +## Help and contact + +- Report issues on [GitHub](https://github.com/affeldt-aist/infotheo/issues) + +## Authors and contributors + +- 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) + diff --git a/infotheo_authors.txt b/infotheo_authors.txt deleted file mode 100644 index 30aed3c4..00000000 --- a/infotheo_authors.txt +++ /dev/null @@ -1,25 +0,0 @@ -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) - -The principle of inclusion-exclusion is a contribution by -Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory) -(main theorem: Pr_bigcup_incl_excl; commit 956096859ed89325b2bb74033690ac882bbcd64e) - -The variable-length source coding theorems are a contribution by -Ryosuke Obi (Chiba U. (M2)) -(commit a67da5e24eaaabb345d225a5bd0f5e86d35413a8) -(with Manabu Hagiwara and Mitsuharu Yamamoto) - -Acknowledgments: -- commit 64814f529c1819684c4b8060d0779c24c6339041 was originally by Karl Palmskog -- The formalization of modern coding theory is a collaboration with -K. Kasai, S. Kuzuoka, R. Obi -- Y. Takahashi collaborated to the formalization of linear error-correcting codes -- This work was partially supported by a JSPS Grant-in-Aid for Scientific -Research (Project Number: 25289118), a JSPS Grand-in-Aid for Scientific Research (Project Number: 18H03204) diff --git a/meta.yml b/meta.yml new file mode 100644 index 00000000..d9e1eb54 --- /dev/null +++ b/meta.yml @@ -0,0 +1,170 @@ +fullname: A Coq formalization of information theory and linear error correcting codes +shortname: infotheo +organization: affeldt-aist +opam_name: coq-infotheo +community: false +action: true +coqdoc: false + +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. +authors: +- name: Reynald Affeldt, AIST + initial: true +- name: Manabu Hagiwara, Chiba U. (previously AIST) + initial: true +- name: Jonas Senizergues, ENS Cachan (internship at AIST) + initial: true +- name: Jacques Garrigue, Nagoya U. + initial: false +- name: Kazuhiko Sakaguchi, Tsukuba U. + initial: false +- name: Taku Asai, Nagoya U. (M2) + initial: false +- name: Takafumi Saikawa, Nagoya U. + initial: false +- name: Naruomi Obata, Titech (M2) + initial: false + +opam-file-maintainer: Reynald Affeldt + +opam-file-version: dev + +license: + fullname: LGPL-2.1-or-later + identifier: LGPL-2.1-or-later + file: LICENSE + +supported_coq_versions: + text: Coq 8.11 to 8.12 + opam: '{ (>= "8.11" & < "8.13~") | (= "dev") }' + +tested_coq_opam_versions: +- version: '1.11.0-coq-8.11' + repo: 'mathcomp/mathcomp' +- version: '1.11.0-coq-8.12' + repo: 'mathcomp/mathcomp' + +dependencies: +- opam: + name: coq-mathcomp-ssreflect + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp ssreflect 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-fingroup + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp fingroup 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-algebra + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp algebra 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-solvable + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp solvable 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-field + version: '{ (>= "1.11.0" & < "1.12~") }' + description: |- + [MathComp field 1.11](https://math-comp.github.io) +- opam: + name: coq-mathcomp-analysis + version: '{ (= "0.3.4") }' + description: |- + [MathComp analysis 0.3.4](https://github.com/math-comp/analysis) +namespace: infotheo + +keywords: +- name: information theory +- name: probability +- name: error-correcting codes + +publications: +- pub_url: https://arxiv.org/abs/2004.12713 + pub_title: Formal Adventures in Convex and Conical Spaces + pub_doi: 10.1007/978-3-030-53518-6_2 +- pub_url: https://link.springer.com/article/10.1007/s10817-019-09538-8 + pub_title: A Library for Formalization of Linear Error-Correcting Codes + pub_doi: 10.1007/s10817-019-09538-8 +- pub_url: https://www.jstage.jst.go.jp/article/jssst/37/3/37_3_79/_article/-char/en + pub_title: Reasoning with Conditional Probabilities and Joint Distributions in Coq + pub_doi: 10.11309/jssst.37.3_79 +- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/compression-isita2018.pdf + pub_title: Examples of formal proofs about data compression + pub_doi: 10.23919/ISITA.2018.8664276 +- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf + pub_title: Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes +- pub_url: http://staff.aist.go.jp/reynald.affeldt/documents/eccITP2015_authorsversion.pdf + pub_title: Formalization of error-correcting codes---from Hamming to modern coding theory + pub_doi: 10.1007/978-3-319-22102-1_2 +- pub_url: https://link.springer.com/article/10.1007%2Fs10817-013-9298-1 + pub_title: Formalization of Shannon’s Theorems + pub_doi: 10.1007/s10817-013-9298-1 + +#make_target: [ +# [make "-j%{jobs}%" ] +# [make "-C" "extraction" "tests"] {with-test} +# ] + +documentation: |- + ## Acknowledgments + + Many thanks to [various contributors](https://github.com/affeldt-aist/infotheo/graphs/contributors) + + The principle of inclusion-exclusion is a contribution by + Erik Martin-Dorel (University Toulouse III Paul Sabatier, IRIT research laboratory) + (main theorem: Pr_bigcup_incl_excl; commit 956096859ed89325b2bb74033690ac882bbcd64e) + + The variable-length source coding theorems are a contribution by + Ryosuke Obi (Chiba U. (M2)) + (commit a67da5e24eaaabb345d225a5bd0f5e86d35413a8) + (with Manabu Hagiwara and Mitsuharu Yamamoto) + + Commit 64814f529c1819684c4b8060d0779c24c6339041 was originally by Karl Palmskog + + The formalization of modern coding theory is a collaboration with + K. Kasai, S. Kuzuoka, R. Obi + + Y. Takahashi collaborated to the formalization of linear error-correcting codes + + This work was partially supported by a JSPS Grant-in-Aid for Scientific + Research (Project Number: 25289118), a JSPS Grand-in-Aid for Scientific Research (Project Number: 18H03204) + + ## Documentation + + Each file is documented in its header. + + Changes are documented in [changelog.txt](changelog.txt). + + ## Installation with Windows 10 (TODO: update) + + Installation of infotheo on Windows is less simple. + See [this page](https://github.com/affeldt-aist/mathcomp-install/blob/master/install-windows-en.org) + for instructions to install MathComp on Windows 10 + (or [this page](https://staff.aist.go.jp/reynald.affeldt/ssrcoq/install.html) for instructions in Japanese). + Once MathComp is installed, two options: + + 1. You have installed MathComp with opam. + Then do: + `opam install coq-infotheo` or `git clone git@github.com:affeldt-aist/infotheo.git; opam install .` + + 2. You have installed MathComp using unzip, untar, cd, make, make install. + Then do: + - Install MathComp-Analysis using unzip, untar, cd, make, make install + + Install bigenough 1.0.0 [download](https://github.com/math-comp/bigenough) + + Install finmap 1.5.0 [download](https://github.com/math-comp/finmap) + + Install analysis 0.3.2 [download](https://github.com/math-comp/analysis) + - Install infotheo using `coq_makefile`, `make`, `make install` as explained above + [download](https://github.com/affeldt-aist/infotheo) + + ## Original License + + Before version 0.2, infotheo was distributed under the terms of the + `GPL-3.0-or-later` license. diff --git a/opam b/opam deleted file mode 100644 index 34e99cc0..00000000 --- a/opam +++ /dev/null @@ -1,44 +0,0 @@ -opam-version: "2.0" -maintainer: "reynald.affeldt@aist.go.jp" -homepage: "https://github.com/affeldt-aist/infotheo" -bug-reports: "https://github.com/affeldt-aist/infotheo/issues" -dev-repo: "git+https://github.com/affeldt-aist/infotheo.git" -license: "LGPL-2.1-or-later" -authors: [ - "Reynald Affeldt" - "Manabu Hagiwara" - "Jonas Senizergues" - "Jacques Garrigue" - "Kazuhiko Sakaguchi" - "Taku Asai" - "Takafumi Saikawa" - "Naruomi Obata" - "Erik Martin-Dorel" - "Ryosuke Obi" - "Mitsuharu Yamamoto" -] -build: [ - [make "-j%{jobs}%"] - [make "-C" "extraction" "tests"] {with-test} -] -install: [ - [make "install"] -] -depends: [ - "coq" {>= "8.11" & < "8.13~"} - "coq-mathcomp-field" {>= "1.11" & < "1.12~"} - "coq-mathcomp-analysis" {>= "0.3.2" & < "0.3.3~"} -] -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. -""" -tags: [ - "category:Computer Science/Data Types and Data Structures" - "keyword: information theory" - "keyword: probability" - "keyword: error-correcting codes" - "logpath:infotheo" - "date:2020-10-13" -]