From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 722157EE99 for ; Mon, 6 Jan 2014 18:43:57 +0100 (CET) X-IronPort-AV: E=Sophos;i="4.95,614,1384297200"; d="scan'208";a="43737609" Received: from wencory.loria.fr (HELO [152.81.3.42]) ([152.81.3.42]) by mail3-relais-sop.national.inria.fr with ESMTP; 06 Jan 2014 18:43:57 +0100 Message-ID: <52CAEB5C.7050206@glondu.net> Date: Mon, 06 Jan 2014 18:43:56 +0100 From: =?ISO-8859-1?Q?St=E9phane_Glondu?= User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20131103 Icedove/17.0.10 MIME-Version: 1.0 To: Michael Ganem CC: caml users References: <52C9A210.2070107@glondu.net> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] [Coq-Club] Compilation of CoQ on Linux 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