# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq dev Formal proof management system
dune 3.0.3 Fast, portable, and opinionated build system
ocaml 4.08.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.08.1 Official release 4.08.1
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.3 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
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.13" & < "8.15~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-algebra" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-solvable" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-field" { (>= "1.13.0" & < "1.14~") | (= "dev") }
"coq-mathcomp-analysis" { (>= "0.3.11") & (< "0.4~")}
]
tags: [
"keyword:information theory"
"keyword:probability"
"keyword:error-correcting codes"
"keyword:convexity"
"logpath:infotheo"
"date:2022-01-03"
]
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)"
]
url {
http: "https://github.com/affeldt-aist/infotheo/archive/0.3.5.tar.gz"
checksum: "sha512=fd70a421ab8a2d506d2328a912621a6d2160c9b0b576a869291772b70d2937066a0b6e471d531d55ed8d5b6e834273412d7f1b1d8a047972894e9a0a86a40695"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.3.5 coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-infotheo.0.3.5 coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-infotheo.0.3.5 coq.dev# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base camlp5 7.14 Preprocessor-pretty-printer of OCaml conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation conf-perl 2 Virtual package relying on perl coq dev Formal proof management system coq-elpi dev Elpi extension language for Coq coq-hierarchy-builder dev High level commands to declare and evolve a hierarchy based on packed classes coq-mathcomp-algebra dev Mathematical Components Library on Algebra coq-mathcomp-analysis 0.3.13 An analysis library for mathematical components coq-mathcomp-bigenough dev A small library to do epsilon - N reasonning coq-mathcomp-field dev Mathematical Components Library on Fields coq-mathcomp-fingroup dev Mathematical Components Library on finite groups coq-mathcomp-finmap dev Finite sets, finite maps, finitely supported functions coq-mathcomp-solvable dev Mathematical Components Library on finite groups (II) coq-mathcomp-ssreflect dev Small Scale Reflection cppo 1.6.8 Code preprocessor like cpp for OCaml dune 3.0.3 Fast, portable, and opinionated build system elpi 1.14.1 ELPI - Embeddable λProlog Interpreter ocaml 4.08.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.08.1 Official release 4.08.1 ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.3 A library manager for OCaml ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_deriving 5.2.1 Type-driven code generation for OCaml ppxlib 0.24.0 Standard library for ppx rewriters re 1.10.3 RE is a regular expression library for OCaml result 1.5 Compatibility Result module seq base Compatibility package for OCaml's standard iterator type starting from 4.07. sexplib0 v0.14.0 Library containing the definition of S-expressions and some base converters stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers [NOTE] Package coq is already installed (current version is dev). The following actions will be performed: - install coq-infotheo 0.3.5 <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/1: [coq-infotheo.0.3.5: http] [coq-infotheo.0.3.5] downloaded from https://github.com/affeldt-aist/infotheo/archive/0.3.5.tar.gz Processing 1/1: <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 1/2: [coq-infotheo: make] + /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-infotheo.0.3.5) - coq_makefile -f _CoqProject -o Makefile.coq - make -f Makefile.coq all - make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-infotheo.0.3.5' - COQDEP VFILES - COQC lib/ssrZ.v - COQC lib/ssrR.v - COQC lib/ssr_ext.v - COQC lib/f2.v - COQC lib/euclid.v - COQC lib/classical_sets_ext.v - File "./lib/ssrR.v", line 596, characters 27-42: - Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. - [deprecated-syntactic-definition,deprecated] - File "./lib/ssrR.v", line 596, characters 27-42: - Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv. - [deprecated-syntactic-definition,deprecated] - File "./lib/ssrR.v", line 599, characters 44-59: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - File "./lib/ssrR.v", line 599, characters 44-59: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - File "./lib/ssrR.v", line 599, characters 44-59: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - COQC ecc_modern/max_subset.v - COQC lib/Reals_ext.v - COQC lib/ssralg_ext.v - COQC lib/num_occ.v - COQC information_theory/kraft.v - COQC ecc_modern/subgraph_partition.v - COQC lib/logb.v - COQC lib/natbin.v - COQC lib/poly_ext.v - COQC lib/vandermonde.v - COQC lib/Ranalysis_ext.v - COQC lib/bigop_ext.v - COQC lib/Rbigop.v - COQC lib/binary_entropy_function.v - COQC ecc_modern/tanner.v - COQC lib/hamming.v - COQC probability/fdist.v - COQC ecc_modern/summary.v - COQC ecc_modern/tanner_partition.v - COQC probability/proba.v - COQC ecc_modern/degree_profile.v - COQC lib/dft.v - COQC probability/jfdist.v - COQC probability/bayes.v - COQC information_theory/source_code.v - COQC toy_examples/expected_value_variance.v - COQC toy_examples/expected_value_variance_ordn.v - COQC toy_examples/expected_value_variance_tuple.v - COQC probability/convex.v - COQC probability/graphoid.v - File "./probability/convex.v", line 1773, characters 46-56: - Warning: Notation prod_curry is deprecated since 8.13. Use uncurry instead. - [deprecated-syntactic-definition,deprecated] - File "./probability/convex.v", line 1781, characters 69-79: - Warning: Notation prod_curry is deprecated since 8.13. Use uncurry instead. - [deprecated-syntactic-definition,deprecated] - File "./probability/convex.v", line 1781, characters 69-79: - Warning: Notation prod_curry is deprecated since 8.13. Use uncurry instead. - [deprecated-syntactic-definition,deprecated] - File "./probability/convex.v", line 1781, characters 69-79: - Warning: Notation prod_curry is deprecated since 8.13. Use uncurry instead. - [deprecated-syntactic-definition,deprecated] - COQC probability/fsdist.v - COQC probability/convex_stone.v - COQC probability/jensen.v - COQC probability/ln_facts.v - COQC probability/divergence.v - COQC probability/variation_dist.v - COQC probability/log_sum.v - File "./probability/divergence.v", line 91, characters 10-19: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/divergence.v", line 91, characters 10-19: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/divergence.v", line 91, characters 10-19: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/divergence.v", line 122, characters 12-21: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/divergence.v", line 122, characters 12-21: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/divergence.v", line 122, characters 12-21: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - COQC information_theory/entropy.v - COQC information_theory/chap2.v - COQC information_theory/aep.v - COQC information_theory/shannon_fano.v - COQC information_theory/string_entropy.v - COQC information_theory/source_coding_vl_converse.v - File "./information_theory/string_entropy.v", line 100, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/string_entropy.v", line 100, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/string_entropy.v", line 100, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - COQC probability/convex_equiv.v - COQC probability/partition_inequality.v - COQC probability/necset.v - COQC information_theory/typ_seq.v - File "./probability/necset.v", line 797, characters 0-155: - Warning: Variables F, i and n do not occur in the right-hand side. The - notation will not be used for printing as it is not reversible. - [non-reversible-notation,parsing] - COQC probability/pinsker.v - COQC information_theory/channel.v - COQC information_theory/convex_fdist.v - File "./probability/pinsker.v", line 78, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/pinsker.v", line 78, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/pinsker.v", line 78, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/pinsker.v", line 81, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/pinsker.v", line 81, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./probability/pinsker.v", line 81, characters 8-17: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - COQC information_theory/source_coding_vl_direct.v - COQC toy_examples/conditional_entropy.v - COQC information_theory/pproba.v - File "./information_theory/source_coding_vl_direct.v", line 295, characters 8-23: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_vl_direct.v", line 295, characters 8-23: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_vl_direct.v", line 295, characters 8-23: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_vl_direct.v", line 380, characters 50-65: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_vl_direct.v", line 380, characters 50-65: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_vl_direct.v", line 380, characters 50-65: - Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult. - [deprecated-syntactic-definition,deprecated] - COQC information_theory/channel_code.v - COQC information_theory/source_coding_fl_direct.v - COQC information_theory/source_coding_fl_converse.v - COQC information_theory/joint_typ_seq.v - File "./information_theory/source_coding_fl_direct.v", line 223, characters 30-39: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_fl_direct.v", line 223, characters 30-39: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_fl_direct.v", line 223, characters 30-39: - Warning: Notation Rinv_Rdiv is deprecated since 8.16. Use Rinv_div. - [deprecated-syntactic-definition,deprecated] - COQC information_theory/erasure_channel.v - File "./information_theory/source_coding_fl_converse.v", line 66, characters 30-36: - Warning: Notation P_Rmin is deprecated since 8.16. Use Rmin_case instead. - [deprecated-syntactic-definition,deprecated] - File "./information_theory/source_coding_fl_converse.v", line 66, characters 30-36: - Warning: Notation P_Rmin is deprecated since 8.16. Use Rmin_case instead. - [deprecated-syntactic-definition,deprecated] - COQC information_theory/binary_symmetric_channel.v - COQC information_theory/types.v - COQC information_theory/channel_coding_direct.v - COQC ecc_classic/decoding.v - COQC information_theory/jtypes.v - COQC ecc_classic/linearcode.v - File "./ecc_classic/linearcode.v", line 827, characters 0-129: - Warning: decoder_coercion does not respect the uniform inheritance condition - [uniform-inheritance,typechecker] - COQC information_theory/conditional_divergence.v - COQC ecc_classic/mceliece.v - COQC ecc_classic/cyclic_code.v - COQC ecc_classic/hamming_code.v - COQC ecc_classic/repcode.v - COQC ecc_modern/checksum.v - COQC ecc_modern/ldpc_erasure.v - COQC information_theory/error_exponent.v - COQC information_theory/success_decode_bound.v - COQC ecc_classic/poly_decoding.v - COQC ecc_modern/summary_tanner.v - COQC ecc_modern/stopping_set.v - COQC information_theory/channel_coding_converse.v - COQC ecc_classic/grs.v - COQC ecc_modern/ldpc.v - COQC ecc_classic/reed_solomon.v - COQC ecc_classic/bch.v - COQC ecc_classic/alternant.v - COQC ecc_modern/ldpc_algo.v - File "./ecc_modern/ldpc_algo.v", line 3, characters 0-31: - Error: Required library Wf matches several files in path (found - /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/theories/Program/Wf.vo and - /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/theories/Init/Wf.vo). - - make[2]: *** [Makefile.coq:793: ecc_modern/ldpc_algo.vo] Error 1 - make[2]: *** Waiting for unfinished jobs.... - make[1]: *** [Makefile.coq:410: all] Error 2 - make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-infotheo.0.3.5' - make: *** [Makefile:2: all] Error 2 [ERROR] The compilation of coq-infotheo failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4". #=== ERROR while compiling coq-infotheo.0.3.5 =================================# # context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.08.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-infotheo.0.3.5 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j4 # exit-code 2 # env-file ~/.opam/log/coq-infotheo-29034-335865.env # output-file ~/.opam/log/coq-infotheo-29034-335865.out ### output ### # [...] # COQC ecc_classic/alternant.v # COQC ecc_modern/ldpc_algo.v # File "./ecc_modern/ldpc_algo.v", line 3, characters 0-31: # Error: Required library Wf matches several files in path (found # /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/theories/Program/Wf.vo and # /home/bench/.opam/ocaml-base-compiler.4.08.1/lib/coq/theories/Init/Wf.vo). # # make[2]: *** [Makefile.coq:793: ecc_modern/ldpc_algo.vo] Error 1 # make[2]: *** Waiting for unfinished jobs.... # make[1]: *** [Makefile.coq:410: all] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.08.1/.opam-switch/build/coq-infotheo.0.3.5' # make: *** [Makefile:2: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-infotheo 0.3.5 +- - No changes have been performed # Run eval $(opam env) to update the current shell environment 'opam install -y -v coq-infotheo.0.3.5 coq.dev' failed.
No files were installed.
true