--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on July 2012 ---
Please ignore the warnings about PVS, and also about the Coq library Floats : the latter is superseded by Flocq, that you already have. - Claude On 07/25/2012 02:46 PM, DAHAN Mickael wrote: > > During the installation of Why-2.31 the following problems appear: > > ... > > checking Coq version... 8.3pl4 > > checking Coq floating-point library... yes > > checking Coq legacy floating-point library... no > > checking for why3... why3 > > checking Coq realizations for Why3... yes > > checking for pvs... /sbin/pvs > > File descriptor 5 (/home/Perco/Users/dahan/why-2.31/config.log) leaked > on pvs invocation. Parent PID 733: /bin/sh > > File descriptor 6 (/dev/pts/6) leaked on pvs invocation. Parent PID > 733: /bin/sh > > File descriptor 7 (/dev/pts/6) leaked on pvs invocation. Parent PID > 733: /bin/sh > > /dev/mapper/control: open failed: Permission denied > > Failure to communicate with kernel device-mapper driver. > > WARNING: Running as a non-root user. Functionality may be unavailable. > > pvs: invalid option -- 'w' > > Error during parsing of command line. > > configure: WARNING: PVS found but pvs -where did not work > > checking for mizf... no > > configure: WARNING: Cannot find Mizar. > > configure: creating ./config.status > > config.status: creating Makefile > > config.status: creating bench/bench > > Summary > > ----------------------------------------- > > OCaml version : 3.12.0 > > OCaml library path : /usr/lib64/ocaml > > OcamlGraph lib : in Ocaml lib, subdir ocamlgraph > > Verbose make : no > > Inference of annotations : no > > Frama-C plugin : yes > > Frama-C version : Nitrogen-20111001 > > GWhy : yes > > Coq support : yes > > Version : v8.1 (8.3pl4) > > Lib : /usr/local/lib/coq > > FP lib (Flocq) : yes > > FP lib (Float) : no (Coq library AllFloat.vo not found) > > PVS support : no > > Mizar support : no > > Other provers support : at run-time (use why-config to configure) > > *Moreover, I can't find **on internet****"coq library AllFloat.vo " .* > > [@@THALES GROUP RESTRICTED@@] > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120726/8c4c1572/attachment.html>