[Why3-club] plugins on OS X

François Bobot bobot at lri.fr
Fri Feb 3 17:12:17 CET 2012


On 03/02/2012 09:20, Alan Schmitt wrote:
> Hello,
>
> Preparing for an upcoming course on Why 3 I installed it on my machine,
> using godi. When I run
> why3config --detect
> I get an error at the end:
>
> == Found /Users/schmitta/godi/lib/why3/whytptp.cmxs ==
> The plugin /Users/schmitta/godi/lib/why3/whytptp.cmxs dynlink failed :
> anomaly: File "src/config.ml", line 13, characters 27-33: Assertion failed
>
> Is there an issue with using plugins on OS X Lion (it seems that native
> dynlink does not work)? If so, does this remove much functionality of
> Why3? Is there a way to compile the plugins in the program?

No important parts are in plugins. 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 think
./configure --disable-whytptp --disable-plugins
with release 0.71 should do the job.

Sorry for the inconvenience,

-- 
François



More information about the Why3-club mailing list