# 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.06.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.06.1 Official 4.06.1 release
ocaml-config 1 OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler
ocamlfind 1.9.1 A library manager for OCaml
ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind
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.06.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.06.1 Official 4.06.1 release ocaml-compiler-libs v0.12.4 OCaml compiler libraries repackaged ocaml-config 1 OCaml Switch Configuration ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler ocamlfind 1.9.1 A library manager for OCaml ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind ppx_derivers 1.2.1 Shared [@@deriving] plugin registry ppx_deriving 5.2.1 Type-driven code generation for OCaml ppxlib 0.25.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 0.2.2 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.06.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.06.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 - COQC ecc_modern/max_subset.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 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 - File "./lib/ssralg_ext.v", line 503, characters 37-51: - Error: - In environment - F : fieldType - The term "mem [char F]" has type "mem_pred nat" - while it is expected to have type - "mem_pred (GRing.Zmodule.sort (GRing.Ring.zmodType ?t))". - - make[2]: *** [Makefile.coq:793: lib/ssralg_ext.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.06.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.06.1 | file:///home/bench/run/opam-coq-archive/released # path ~/.opam/ocaml-base-compiler.4.06.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-24994-335865.env # output-file ~/.opam/log/coq-infotheo-24994-335865.out ### output ### # [...] # Error: # In environment # F : fieldType # The term "mem [char F]" has type "mem_pred nat" # while it is expected to have type # "mem_pred (GRing.Zmodule.sort (GRing.Ring.zmodType ?t))". # # make[2]: *** [Makefile.coq:793: lib/ssralg_ext.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.06.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