--- layout: fc_discuss_archives title: Message 17 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



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                    |