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 GNU make. Error: Unable to locate library Rstruct with prefix mathcomp. #54

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: git clone https://github.com/affeldt-aist/infotheo.git cd infotheo make

Outputs: make -f Makefile.coq all make[1]: Entering directory '/home/user/Documents/infotheo' COQC lib/ssrR.v File "./lib/ssrR.v", line 5, characters 29-36: Error: Unable to locate library Rstruct with prefix mathcomp.

make[2]: [Makefile.coq:720: lib/ssrR.vo] Error 1 make[1]: [Makefile.coq:343: all] Error 2 make[1]: Leaving directory '/home/user/Documents/infotheo' make: *** [Makefile:2: all] Error 2

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?

I don't understand why it fails. coq-mathcomp-analysis does install Rstruct.vo in user-contrib inside the mathcomp directory and Rstruct.v has not been modified recently. It compiles on my machine (same version of Ubuntu) with the same dependencies.