Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Dependency of ocaml version on why3-0.83

Hi,

It seems you have used Opam to install OCaml. You should do the same thing
for Jessie and Why3, by installing respectively the why and why3 packages.
If you are not root, install your own version of Opam. It will make things
simpler in the end.

HTH,

On Thu, Jul 14, 2016 at 8:17 AM, Prasuna Saka <prasuna.drdo at gmail.com>
wrote:

> Hi,
>
> I am having FRAMA-C Version:Neon-20140301 installed. Want to install
> Jessie Plug-in. As per the dependency tree listed in the web page of
> Krakatoa and Jessie  , compatible Why version is 2.34, which got installed
> successfully. However, when trying to install Why3-0.83 , following error
> is thrown:
>
> Output of running configure command:
>
> Verbose make            : no
> OCaml compiler          : yes
>     Version             : 4.02.3
>     Library path        : /root/.opam/4.02.3/lib/ocaml
>     Native compilation  : yes
>     Profiling           : no
> Zarith                  : yes
> IDE                     : yes
> Bench tool              : no (sqlite3 not found)
> Documentation           : no (rubber not found)
> Coq support             : no (version is 8.5pl2 but need version 8.4 or
> higher)
> PVS support             : no (pvs not found)
> Isabelle support        : no (isabelle not found)
> Frama-C support         : no (disabled by default)
> Hypothesis selection    : yes
> Installable             : yes
>     Binary path         : ${exec_prefix}/bin
>     Lib path            : ${exec_prefix}/lib/why3
>     Data path           : ${prefix}/share/why3
>     Ocaml Library       : /root/.opam/4.02.3/lib/why3
>     Relocatable         : no
>
> Error with make command:
>
> Error: src/util/debug.cmi
> is not a compiled interface for this version of OCaml.
> It seems to be for an older version of OCaml.
> Makefile:1685: recipe for target 'src/driver/call_provers.cmx' failed
> make: *** [src/driver/call_provers.cmx] Error 2
>
> May I please know what is this error for and how to resolve it?
>
> Thanks
> Prasuna
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>



-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160714/30c4b470/attachment.html>