Re: [Caml-list] [Coq-Club] Compilation of CoQ on Linux

Re: [Caml-list] [Coq-Club] Compilation of CoQ on Linux

[Stéphane Glondu]

Le 06/01/2014 09:08, Michael Ganem a écrit :
> I run the compilation again in byte code and get a bit more verbose error:
> OCAMLC -a -o plugins/syntax/string_syntax_plugin.cma
> COQMKTOP -o bin/coqtop.byte
> COQC -nois theories/Init/Notations.v
> Fatal error: cannot load shared library dllcoqrun
> Reason: dllcoqrun.so: cannot open shared object file: No such file or
> directory
> make[1]: *** [theories/Init/Notations.vo] Error 2
> make[1]: Leaving directory `/coq'
> make: *** [world] Error 2

This error is different. Try after running ./configure with the "-local"
option, "make clean", then "make".

> I'm trying to compile coq-8.4pl3.tar.gz but I tried also 8.3 and I get the
> same result. My linux system is a bit peculiar, it is a ubuntu distribution
> compiled on ARM.
> apt-get install does not find the package for this architecture.

So I guess your error is the same as:


https://launchpadlibrarian.net/154174407/buildlog_ubuntu-trusty-armhf.coq_8.4pl2dfsg-1_FAILEDTOBUILD.txt.gz

In the development version of Ubuntu (Trusty Tahr), the coq package is
compiled on all architectures:

  https://launchpad.net/ubuntu/+source/coq/8.4pl2dfsg-4

My first guess would be a broken native compiler that was fixed later,
so your approach to compile in bytecode only is a good idea. You could
also use a chroot with coq and its dependencies installed from trusty.


Cheers,

-- 
Stéphane