coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: plugins, native code, ppc, v8.2

From: Damien Pous <Damien.Pous AT ens-lyon.fr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Re: plugins, native code, ppc, v8.2
Date: Thu, 18 Feb 2010 12:44:09 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type; b=BUukvOzf5V0B3pD5YlJH58qXtw2cfWkML+5j2ZhQ7Qr5Anf5stcKs5XfYFhUhCLDND EsYJevEJaVusgjxmn2cue6s66Wxswqreuq9CzYUA2jmnlZUD4jlvZswsgETM7wP8WPSx eaSs/6EZ9sXbmstH6O5cR7Nnzk8QxQoADBxaQ=

I just realised that this limitation was already known :
http://coq.inria.fr/bugs/show_bug.cgi?id=2023
(I was looking only at *open* bugs, this morning...)

Two notes:
- dynlink seems to work fine on Intel, with xcode 3.1.3, ocaml 3.11 :
the problem arises with PPC only
- the v8.3 does not compile on PPC, for the same reasons as previously
: we have to give the '-natdynlink no' option to the configure script.
Maybe the configure script should detect PPC architectures and
disallow natdynlink automatically.

Best,
Damien

[Coq-Club] plugins, native code, ppc, v8.2, Damien Pous
- [Coq-Club] Re: plugins, native code, ppc, v8.2, Damien Pous