[Why3-club] plugins on OS X
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
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.
More information about the Why3-club