[Why3-club] plugins on OS X

François Bobot bobot at lri.fr
Fri Feb 3 19:32:40 CET 2012


On 03/02/2012 10:20, Alan Schmitt wrote:
> On 3 Feb 2012, at 17:12, François Bobot wrote:
>
>> No important parts are in plugins.
>
> Great, good to know.
>
>> It's strange the configure detect that your ocaml version don't have
>> native plugins and your ocaml version is able to compile one. Now why3
>> trunk requires ocaml 3.11.2. Thus no more question about native
>> dynlink (by the way can you try with the trunk?)
>
> I can, but I want to make sure this is not a typo: I'm running 3.12.1. I
> would need to downgrade to 3.11.2 for why3 trunk?

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 think
>> ./configure --disable-whytptp --disable-plugins
>> with release 0.71 should do the job.
>
> 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?

>
> 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?

I hope that now work fine.

-- 
François



More information about the Why3-club mailing list