--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on July 2016 ---
Mr. Claude, Thanks for your helpful note on my queries. Now I think I have more or less done with the installation. As you said, I have done the following: -- Installed opam -- opam install ocaml -- opam install why with the above commands, ocaml version 4.02.3, FRAMA-C version sodium-20150201 why3 version 0.85 have got installed successfully. I could launch the GUI as well ( with the command frama-c -jessie testpgm.c).Since no provers are installed a message to run why3 congig --detect-provers is popped. I have installed Alt-Ergo SMT solver using the command "opam install alt-ergo". Then, alt-ergo version 0.991 version has got installed. With the command why3 config --detect then, this it shown that this version of alt-ergo is not supported. Same is happening with the coq Prover as well. How do I find which version of the external provers will be supported by my current configuration.? Do I need to install all the provers with opam or can I use sudo apt-get install command? I wanted to work with Coq prover , as I have a C Program involving floats and trigonometric functions to be verified. Thanks & Regards Prasuna On Mon, Jul 18, 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: Frama-c-discuss Digest, Vol 97, Issue 9 (Claude Marché) > 2. Re: Installing Jessie plugin (Claude Marché) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 18 Jul 2016 09:09:30 +0200 > From: Claude Marché <Claude.Marche at inria.fr> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] Frama-c-discuss Digest, Vol 97, Issue 9 > Message-ID: <578C80AA.8040500 at inria.fr> > Content-Type: text/plain; charset=utf-8 > > > 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 | > > > ------------------------------ > > Message: 2 > Date: Mon, 18 Jul 2016 09:11:13 +0200 > From: Claude Marché <Claude.Marche at inria.fr> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] Installing Jessie plugin > Message-ID: <578C8111.2070706 at inria.fr> > Content-Type: text/plain; charset=utf-8 > > > > Le 15/07/2016 11:40, Prasuna Saka a écrit : > > Having FRAMAC Neon version installed, trying to install jessie plug-in, > > getting into the following problem. > > > > Chosen Why3-0.83 and why2-35. > > please be careful with the dependencies : see http://krakatoa.lri.fr/ > > however, as I said before with opam the proper dependencies should be > chosen for you. > > - Claude > > > > -- > 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 | > > > ------------------------------ > > 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 11 > *********************************************** > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160719/fcc59812/attachment-0001.html>