[Why3-club] plugins on OS X

Alan Schmitt alan.schmitt at polytechnique.org
Sat Feb 4 09:27:10 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

Compilation fails on the trunk. Here is what configure returns:

OCaml version           : 3.12.1
OCaml library path      : /Users/schmitta/godi/lib/ocaml/std-lib
Verbose make            : no
Why IDE                 : yes
Why bench tool          : yes
Why documentation       : no
Coq support             : yes
     Version             : 8.3pl2
     Lib                 : /Users/schmitta/godi/lib/coq
     Plugin support      : no  (not yet implemented)
     Realization support : yes
         FP arithmetic   : yes
TPTP parser             : yes
Menhir library          : no
hypothesis selection    : yes
profiling               : no
localdir                : no

But the linking at the end fails:

Linking  bin/why3.opt
File "_none_", line 1, characters 0-1:
Error: Cannot find file dynlink.cmxa
make: *** [bin/why3.opt] Error 2


More information about the Why3-club mailing list