--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on July 2012 ---
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@@] -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120725/8a0563fb/attachment.html>