search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

Unable to install using opam. ERROR while compiling coq-infotheo.0.3.1 #55

Closed ievajas closed 3 years ago

ievajas commented 3 years ago

Ubuntu 20.04.2 LTS Release: 20.04

opam --version 2.0.5

coqc --version The Coq Proof Assistant, version 8.13.1 (March 2021) compiled on Mar 8 2021 11:40:26 with OCaml 4.08.1

opam list mathcomp

Name Installed Synopsis coq-mathcomp-algebra 1.12.0 Mathematical Components Library on Algebra coq-mathcomp-analysis 0.3.6 An analysis library for mathematical components coq-mathcomp-bigenough 1.0.0 A small library to do epsilon - N reasonning coq-mathcomp-field 1.12.0 Mathematical Components Library on Fields coq-mathcomp-fingroup 1.12.0 Mathematical Components Library on finite groups coq-mathcomp-finmap 1.5.1 Finite sets, finite maps, finitely supported functions coq-mathcomp-solvable 1.12.0 Mathematical Components Library on finite groups (II) coq-mathcomp-ssreflect 1.12.0 Small Scale Reflection

Running: opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-infotheo

Outputs:

`` The following actions will be performed: ∗ install coq-infotheo 0.3.1

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [coq-infotheo.0.3.1] found in cache

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> [ERROR] The compilation of coq-infotheo failed at "/home/user/.opam/opam-init/hooks/sandbox.sh build make -j1".

#=== ERROR while compiling coq-infotheo.0.3.1 =================================# # context 2.0.5 | linux/x86_64 | ocaml-base-compiler.4.11.1 | https://coq.inria.fr/opam/released#2021-03-22 11:00 # path ~/.opam/with-coq/.opam-switch/build/coq-infotheo.0.3.1 # command ~/.opam/opam-init/hooks/sandbox.sh build make -j1 # exit-code 2 # env-file ~/.opam/log/coq-infotheo-51929-d2c37b.env # output-file ~/.opam/log/coq-infotheo-51929-d2c37b.out ### output ### # [...] # Warning: filter_index_enum is deprecated; use big_enumP instead # Warning: filter_index_enum is deprecated; use big_enumP instead # Warning: filter_index_enum is deprecated; use big_enumP instead # COQC toy_examples/expected_value_variance.v # COQC toy_examples/expected_value_variance_ordn.v # COQC toy_examples/expected_value_variance_tuple.v # COQC toy_examples/conditional_entropy.v # Killed # make[2]: *** [Makefile.coq:720: toy_examples/conditional_entropy.vo] Error 137 # make[1]: *** [Makefile.coq:343: all] Error 2 # make[1]: Leaving directory '/home/user/.opam/with-coq/.opam-switch/build/coq-infotheo.0.3.1' # make: *** [Makefile:2: all] Error 2

<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> ┌─ The following actions failed │ λ build coq-infotheo 0.3.1 └─ ╶─ No changes have been performed # Run eval $(opam env) to update the current shell environment

`` Could anyone help to figure out and solve the issue?

affeldt-aist commented 3 years ago

Could anyone help to figure out and solve the issue?

It looks like it was about to succeed. COQC toy_examples/conditional_entropy.v is the last action. However, it is true that the compilation of this file is a bit long.

ievajas commented 3 years ago

Solved by first installing Elpi (opam install elpi), and then repeating the steps.