--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on July 2016 ---
Dear Prasuna, I must admit I don't understand your problem. with a fresh opam installation simply typing opam install why should install everything needed, including the dependencies Frama-C and why3. I wonder if you are not trying to install why3 again after installing why: this is wrong, you should not do that. Why depend on Why3, not the other way around. Otherwise, please try to report the problem more clearly with a detailed log of what happens for you. - Claude Le 15/07/2016 15:17, Prasuna Saka a écrit : > 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 > <mailto: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 > <mailto: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 > <mailto: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 > <mailto: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 > <mailto:boris at yakobowski.org>> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr > <mailto: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 > <mailto: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 <mailto: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 > <mailto: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 > <mailto:prasuna.drdo at gmail.com>> > To: frama-c-discuss at lists.gforge.inria.fr > <mailto: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 > <mailto: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 <http://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 > <mailto: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 > ********************************************** > > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Ãle-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |