--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on July 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 9



Hi,

Thhnks for the reply

If I install why and why3 with opam , provided ocaml is installed using
spam then latest why3 version- why3-0.87 is installed which is not
supported by the FRAMA_C version i am having. How do I really install the
required why3 and why version using opam.

Hope my question is clear.

I have tried to install everything in the other way as well, i.e without
using opam:

Firstly, ocaml version 4.02.3 is installed and when why3-0.83 is tried for
installing, error thrown for the make command.

Do not know what to do now!


Thanks
Prasuna

On Fri, Jul 15, 2016 at 3:30 PM, <
frama-c-discuss-request at lists.gforge.inria.fr> wrote:

> Send Frama-c-discuss mailing list submissions to
>         frama-c-discuss at lists.gforge.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> or, via email, send a message with subject or body 'help' to
>         frama-c-discuss-request at lists.gforge.inria.fr
>
> You can reach the person managing the list at
>         frama-c-discuss-owner at lists.gforge.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Frama-c-discuss digest..."
>
>
> Today's Topics:
>
>    1. Re: Dependency of ocaml version on why3-0.83 (Boris Yakobowski)
>    2. Installing Jessie plugin (Prasuna Saka)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Thu, 14 Jul 2016 15:21:43 +0200
> From: Boris Yakobowski <boris at yakobowski.org>
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Subject: Re: [Frama-c-discuss] Dependency of ocaml version on
>         why3-0.83
> Message-ID:
>         <CABbVA-D=8yoc4e1kB0dzqVyaLs5GKFL-pKAm=
> h9ueuyU3vTCGQ at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> 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-0001.html
> >
>
> ------------------------------
>
> Message: 2
> Date: Fri, 15 Jul 2016 15:10:27 +0530
> From: Prasuna Saka <prasuna.drdo at gmail.com>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: [Frama-c-discuss] Installing Jessie plugin
> Message-ID:
>         <CAA80GKO364LP85DZw9kG=
> MnzB748ftseUDSq_WvP6zd5Zu-vxQ at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> Having FRAMAC Neon version installed, trying to install jessie plug-in,
> getting into the following problem.
>
> Chosen Why3-0.83 and why2-35.
>
> While installing why3, following is the issue:
>
> output of configure command is :
>
> Verbose make            : no
> OCaml compiler          : yes
>     Version             : 4.02.3
>     Library path        : /usr/local/lib/ocaml
>     Native compilation  : yes
>     Profiling           : no
> Zarith                  : no (zarith not found)
> IDE                     : no (lablgtk2 not found)
> Bench tool              : no (sqlite3 not found)
> Documentation           : no (rubber not found)
> Coq support             : yes
>     Version             : 8.4pl4
>     Library path        : /usr/lib/coq
>     "why3" tactic       : no (/usr/lib/coq/kernel/term.cmi not found)
>     Realization support : yes
>         FP arithmetic   : no (Flocq >= 2.2 not found)
> PVS support             : no (pvs not found)
> Isabelle support        : no (isabelle not found)
> Frama-C support         : no (disabled by default)
> Hypothesis selection    : no (ocamlgraph not found)
> Installable             : yes
>     Binary path         : ${exec_prefix}/bin
>     Lib path            : ${exec_prefix}/lib/why3
>     Data path           : ${prefix}/share/why3
>     Ocaml Library       : /usr/local/lib/ocaml/why3
>     Relocatable         : no
>
> With make command, following is the error thrown:
>
> File "src/driver/call_provers.ml", line 1:
> 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
>
> Please, help me out to solve this.
>
> Regards,
> Prasuna
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160715/5dbf5771/attachment-0001.html
> >
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
> ------------------------------
>
> End of Frama-c-discuss Digest, Vol 97, Issue 9
> **********************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160715/0a0ebf02/attachment.html>