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] Frama-c-discuss Digest, Vol 97, Issue 9

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 9
  • From: prasuna.drdo at gmail.com (Prasuna Saka)
  • Date: Fri, 15 Jul 2016 18:47:11 +0530
  • In-reply-to: <mailman.15.1468576808.11482.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.15.1468576808.11482.frama-c-discuss@lists.gforge.inria.fr>
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>