--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on July 2012 ---
During the installation of Why3 O.72 the following problems appear: typed commands: tar -xvzf why3-0.72.tar.gz cd why3-0.72 ./configure --enable-coq-plugin --enable-coq-libs make results: Summary ----------------------------------------- OCaml version : 3.12.0 OCaml library path : /usr/lib64/ocaml Compile in native code : yes Verbose make : no Why IDE : yes Why bench tool : no Why documentation : no Coq support : yes Version : 8.4beta2 Lib : /usr/local/lib/coq Plugin support : yes Realization support : yes FP arithmetic : yes hypothesis selection : yes debugging symbols : no profiling : no localdir : no ... Ocamlopt src/ide/gconfig.ml Ocamlopt src/ide/gmain.ml Linking bin/why3ide.opt Ocamlopt src/ide/replay.ml Linking bin/why3replayer.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml Ocamlopt src/why3session/why3session_copy.ml Ocamlopt src/why3session/why3session_info.ml Ocamlopt src/why3session/why3session_latex.ml Ocamlopt src/why3session/why3session_html.ml Ocamlopt src/why3session/why3session_rm.ml Ocamlopt src/why3session/why3session.ml Linking bin/why3session.opt Ocamlopt src/coq-tactic/why3tac.ml File "src/coq-tactic/why3tac.ml", line 477, characters 14-20: Error: This pattern matches values of type 'a option but a pattern was expected which matches values of type Declarations.constant_def make: *** [src/coq-tactic/why3tac.cmx] Error 2 [@@THALES GROUP RESTRICTED@@] De : frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la part de Claude Marche Envoy? : vendredi 20 juillet 2012 21:13 ? : frama-c-discuss at lists.gforge.inria.fr Objet : Re: [Frama-c-discuss] Plateform Why3 0.72 On 07/20/2012 10:20 AM, DAHAN Mickael wrote: Hello. I would like to know how can I do to launch the plateform Why3 0.72 on frama-c Nitrogen. The formulation of your question is somewhat strange... Please see http://krakatoa.lri.fr for explanations on the relations between Frama-C, Why3, and the Jessie plugin. In short: * compile and install Frama-C Nitrogen and Why3 in any order (the newer Why3 0.73 if possible ;-) * compile and install Why 2.31 which contains the Jessie plugin * detect provers: why3config --detect then: frama-c -jessie file.c will start compute VCs for your C code and start the why3 GUI on them - Claude -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120723/32b96069/attachment.html>