[Why3-club] Compilation error with coq8.4

Alan Schmitt alan.schmitt at polytechnique.org
Thu Sep 6 19:48:21 CEST 2012


Hi Virgile,

Virgile Prevosto <virgile.prevosto at m4x.org> writes:

> Hello Alan,
>
> 2012/9/6 Johannes Kanig <kanig at adacore.com>:
>> On 09/06/2012 05:18 PM, Alan Schmitt wrote:
>>> I checked and the file why3ml is indeed not there.
>>> ===> Registering installation for apps-why3-0.73godi99
>>
>> AFAIK, the 'why3ml' executable was removed, and got replaced by 'why3'.
>> So I suspect the error is in the godi driver.
>
> Well, on my plain 0.73 install I still have it. However, the godi99
> suffix in the log indicates that you're compiling the git version, in
> which case I trust Johannes to be right (the godi package is supposed
> to work with vanilla distribution, users brave enough to use the
> development version have to live with a less stable environment ;-).
>
> The easiest fix is to remove bin/why3ml from the PLIST file in
> ${GODI_HOME}/build/apps/apps-why3 (or set CONF_WHY3_GIT to no)

Thanks, that was it: I set CONF_WHY3_GIT to no and it worked.

Unfortunately it does not build the IDE, because lablgtksourceview is
not found:

> checking for /Users/schmitta/godi/lib/ocaml/std-lib/lablgtk2/lablgtksourceview2.cma... no

The problem is that it's looking for it in the wrong place. It's in fact
in

/Users/schmitta/godi/lib/ocaml/pkg-lib/lablgtk2/lablgtksourceview2.cma

(std-lib should be replaced by pkg-lib).

Thanks again,

Alan



More information about the Why3-club mailing list