From: "Stéphane Glondu" <steph@glondu.net>
To: Michael Ganem <michael.ganem@gmail.com>
Cc: caml users <caml-list@inria.fr>
Subject: Re: [Caml-list] [Coq-Club] Compilation of CoQ on Linux
Date: Mon, 06 Jan 2014 18:43:56 +0100 [thread overview]
Message-ID: <52CAEB5C.7050206@glondu.net> (raw)
In-Reply-To: <CACQs58xfb3p+hbvXOzEtsxZidG_4mS15Jo_B-6pK4HbtPCk9=A@mail.gmail.com>
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
parent reply other threads:[~2014-01-06 17:43 UTC|newest]
Thread overview: expand[flat|nested] mbox.gz Atom feed
[parent not found: <CACQs58xfb3p+hbvXOzEtsxZidG_4mS15Jo_B-6pK4HbtPCk9=A@mail.gmail.com>]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=52CAEB5C.7050206@glondu.net \
--to=steph@glondu.net \
--cc=caml-list@inria.fr \
--cc=michael.ganem@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).