[Why3-club] plugins on OS X

Alan Schmitt alan.schmitt at polytechnique.org
Fri Feb 3 20:48:17 CET 2012


On 3 Feb 2012, at 19:32, François Bobot wrote:

> Sorry, it requires *at least* 3.11.2. 3.12.1 is just fine. If you have 
> 3.12.1 I don't understand the bug which occurs. Have you been able to 
> compile the trunk? Just in order to be sure that will work for the 
> next release.
>
> git clone git://scm.gforge.inria.fr/why3/why3.git

I'll give it a try, probably this week-end.

>> I used the default configuration option, which seems to say that 
>> dynlink
>> should work on my system while it doesn't. I'm now compiling with
>> plugins and tptp disabled.
>
> In your previous mail, I though that your version of ocaml has been 
> able to generate a .cmxs?

Yes, it seems the issue is not generating it but loading it. But I may 
be mistaken.

>> Hopefully this will be much better with the next version of caml: if 
>> I
>> understand http://caml.inria.fr/mantis/view.php?id=4863 correctly, OS 
>> X
>> 64bits machines should get native dynlink back.
>
> I don't understand why this bug concerns only dynlink. Which are the 
> version of ocaml for OS X which doesn't work?

 From what I've understood, dynlink worked until 10.5 (included). From 
10.6 on, it required position independent code, which is not generated 
by ocaml. But somehow an option can be used with 64 bits machines that 
make it work.

I want to stress that I'm very much out of my league here: I just 
learned about these issues today and my understanding comes from a few 
minutes of browsing, so I may be completely wrong.

Alan



More information about the Why3-club mailing list