(2021-04-03 04:38:32 UTC)
# 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 3 Virtual package relying on a GMP lib system installation coq dev Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.11.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.11.1 Official release 4.11.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 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.14~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.13~") } "coq-mathcomp-fingroup" { (>= "1.12.0" & < "1.13~") } "coq-mathcomp-algebra" { (>= "1.12.0" & < "1.13~") } "coq-mathcomp-solvable" { (>= "1.12.0" & < "1.13~") } "coq-mathcomp-field" { (>= "1.12.0" & < "1.13~") } "coq-mathcomp-analysis" { (>= "0.3.6") } ] tags: [ "keyword:information theory" "keyword:probability" "keyword:error-correcting codes" "keyword:convexity" "logpath:infotheo" "date:2021-03-23" ] 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.2.tar.gz" checksum: "sha512=ab3a82c343eb3b1fc164e95cc963612310f06a400e3fb9781c28b4afb37356a57a99d236cd788d925ae5f2c8ce8f96850ad40d5a79306daca69db652c268d5f8" }
true
Dry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.3.2 coq.dev
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-infotheo.0.3.2 coq.dev
# 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 3 Virtual package relying on a GMP lib system installation coq dev Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.11.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.11.1 Official release 4.11.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.1 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers The following actions will be performed: - install coq-mathcomp-ssreflect 1.12.0 - install seq base - install dune 2.8.5 - install conf-perl 1 - install coq-mathcomp-fingroup 1.12.0 - install coq-mathcomp-bigenough dev - install sexplib0 v0.14.0 - install result 1.5 - install re 1.9.0 - install ppx_derivers 1.2.1 - install ocaml-compiler-libs v0.12.3 - install cppo 1.6.7 - install camlp5 7.14 - install coq-mathcomp-algebra 1.12.0 - install coq-mathcomp-finmap dev - install csexp 1.4.0 - install ocaml-migrate-parsetree 1.8.0 - install coq-mathcomp-solvable 1.12.0 - install dune-configurator 2.8.5 - install coq-mathcomp-field 1.12.0 - install base v0.14.1 - install stdio v0.14.0 - install ppxlib 0.14.0 - install ppx_deriving 5.1 - install elpi 1.13.0 - install coq-elpi dev - install coq-hierarchy-builder dev - install coq-mathcomp-analysis dev ===== 28 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [base.v0.14.1] downloaded from cache at https://opam.ocaml.org/cache [camlp5.7.14] downloaded from cache at https://opam.ocaml.org/cache [coq-mathcomp-algebra.1.12.0] downloaded from https://github.com/math-comp/math-comp/archive/mathcomp-1.12.0.tar.gz [coq-elpi.dev] synchronised from git+https://github.com/LPCIC/coq-elpi.git#coq-master [coq-hierarchy-builder.dev] synchronised from git+https://github.com/math-comp/hierarchy-builder.git#master [coq-mathcomp-field.1.12.0] found in cache [coq-mathcomp-fingroup.1.12.0] found in cache [coq-mathcomp-analysis.dev] synchronised from git+https://github.com/math-comp/analysis.git#master [coq-mathcomp-solvable.1.12.0] found in cache [coq-mathcomp-ssreflect.1.12.0] found in cache [cppo.1.6.7] downloaded from cache at https://opam.ocaml.org/cache [coq-mathcomp-bigenough.dev] synchronised from git+https://github.com/math-comp/bigenough.git#master [csexp.1.4.0] downloaded from cache at https://opam.ocaml.org/cache [dune.2.8.5] downloaded from cache at https://opam.ocaml.org/cache [dune-configurator.2.8.5] downloaded from cache at https://opam.ocaml.org/cache [coq-mathcomp-finmap.dev] synchronised from git+https://github.com/math-comp/finmap.git#master [ocaml-compiler-libs.v0.12.3] downloaded from cache at https://opam.ocaml.org/cache [elpi.1.13.0] downloaded from cache at https://opam.ocaml.org/cache [ocaml-migrate-parsetree.1.8.0] downloaded from cache at https://opam.ocaml.org/cache [ppx_derivers.1.2.1] downloaded from cache at https://opam.ocaml.org/cache [ppx_deriving.5.1] downloaded from cache at https://opam.ocaml.org/cache [ppxlib.0.14.0] downloaded from cache at https://opam.ocaml.org/cache [re.1.9.0] downloaded from cache at https://opam.ocaml.org/cache [result.1.5] downloaded from cache at https://opam.ocaml.org/cache [sexplib0.v0.14.0] downloaded from cache at https://opam.ocaml.org/cache [stdio.v0.14.0] downloaded from cache at https://opam.ocaml.org/cache <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed seq.base -> installed conf-perl.1 -> installed dune.2.8.5 -> installed cppo.1.6.7 -> installed ocaml-compiler-libs.v0.12.3 -> installed ppx_derivers.1.2.1 -> installed result.1.5 -> installed csexp.1.4.0 -> installed dune-configurator.2.8.5 -> installed re.1.9.0 -> installed sexplib0.v0.14.0 -> installed ocaml-migrate-parsetree.1.8.0 -> installed coq-mathcomp-ssreflect.1.12.0 -> installed base.v0.14.1 -> installed camlp5.7.14 -> installed coq-mathcomp-bigenough.dev -> installed stdio.v0.14.0 -> installed ppxlib.0.14.0 -> installed coq-mathcomp-fingroup.1.12.0 -> installed coq-mathcomp-finmap.dev -> installed ppx_deriving.5.1 -> installed elpi.1.13.0 -> installed coq-mathcomp-algebra.1.12.0 -> installed coq-elpi.dev [ERROR] The compilation of coq-hierarchy-builder failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make". -> installed coq-mathcomp-solvable.1.12.0 -> installed coq-mathcomp-field.1.12.0 #=== ERROR while compiling coq-hierarchy-builder.dev ==========================# # context 2.0.7 | linux/x86_64 | ocaml-base-compiler.4.11.1 | file:///home/bench/run/opam-coq-archive/extra-dev # path ~/.opam/ocaml-base-compiler.4.11.1/.opam-switch/build/coq-hierarchy-builder.dev # command ~/.opam/opam-init/hooks/sandbox.sh build make # exit-code 2 # env-file ~/.opam/log/coq-hierarchy-builder-9962-bbf0fb.env # output-file ~/.opam/log/coq-hierarchy-builder-9962-bbf0fb.out ### output ### # [...] # At least one of the following errors holds: # File "./HB/common/database.elpi", line 254: (cs-instance) has type type but is applied to _ _ (global Inst) # File "./HB/common/database.elpi", line 254: (global Inst) has type term but is used with type gref # # # # make[3]: *** [Makefile.coq:721: structures.vo] Error 1 # make[2]: *** [Makefile.coq:344: all] Error 2 # make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.11.1/.opam-switch/build/coq-hierarchy-builder.dev' # make[1]: *** [Makefile:97: this-build] Error 2 # make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.11.1/.opam-switch/build/coq-hierarchy-builder.dev' # make: *** [Makefile:64: all] Error 2 <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> +- The following actions failed | - build coq-hierarchy-builder dev +- +- The following changes have been performed (the rest was aborted) | - install base v0.14.1 | - install camlp5 7.14 | - install conf-perl 1 | - install coq-elpi dev | - install coq-mathcomp-algebra 1.12.0 | - install coq-mathcomp-bigenough dev | - install coq-mathcomp-field 1.12.0 | - install coq-mathcomp-fingroup 1.12.0 | - install coq-mathcomp-finmap dev | - install coq-mathcomp-solvable 1.12.0 | - install coq-mathcomp-ssreflect 1.12.0 | - install cppo 1.6.7 | - install csexp 1.4.0 | - install dune 2.8.5 | - install dune-configurator 2.8.5 | - install elpi 1.13.0 | - install ocaml-compiler-libs v0.12.3 | - install ocaml-migrate-parsetree 1.8.0 | - install ppx_derivers 1.2.1 | - install ppx_deriving 5.1 | - install ppxlib 0.14.0 | - install re 1.9.0 | - install result 1.5 | - install seq base | - install sexplib0 v0.14.0 | - install stdio v0.14.0 +- # Run eval $(opam env) to update the current shell environment The former state can be restored with: opam switch import "/home/bench/.opam/ocaml-base-compiler.4.11.1/.opam-switch/backup/state-20210402041749.export"
true
No files were installed.
true