[Why3-club] plugins on OS X

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


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?

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

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.

Thanks,

Alan



More information about the Why3-club mailing list