(2021-04-06 20:47:58 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.10.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.1 Official release 4.10.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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-infotheo.0.3.2 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 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.10.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.1 Official release 4.10.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 csexp 1.5.1
- install cppo 1.6.7
- install camlp5 7.14
- install coq-mathcomp-algebra 1.12.0
- install coq-mathcomp-finmap dev
- install ocaml-migrate-parsetree 1.8.0
- install dune-configurator 2.8.5
- install coq-mathcomp-solvable 1.12.0
- install base v0.14.1
- install coq-mathcomp-field 1.12.0
- 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
[csexp.1.5.1] downloaded from cache at https://opam.ocaml.org/cache
[coq-mathcomp-bigenough.dev] synchronised from git+https://github.com/math-comp/bigenough.git#master
[dune.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
[dune-configurator.2.8.5] downloaded from cache at https://opam.ocaml.org/cache
[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 csexp.1.5.1
-> installed ocaml-compiler-libs.v0.12.3
-> installed ppx_derivers.1.2.1
-> installed re.1.9.0
-> installed result.1.5
-> installed dune-configurator.2.8.5
-> 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.6 | linux/x86_64 | ocaml-base-compiler.4.10.1 | file:///home/bench/run/opam-coq-archive/extra-dev
# path ~/.opam/ocaml-base-compiler.4.10.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-17931-bbf0fb.env
# output-file ~/.opam/log/coq-hierarchy-builder-17931-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.10.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.10.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.5.1
| - 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.10.1/.opam-switch/backup/state-20210406175309.export"
trueNo files were installed.
true