--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on July 2012 ---
To install the plateform Why-2.31 I have download the version < coq-8.3pl4 > I would like to know how can i install the following source code: coq-float_8.3pl1.orig.tar.gz ... 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 8173: /bin/sh File descriptor 6 (/dev/pts/6) leaked on pvs invocation. Parent PID 8173: /bin/sh File descriptor 7 (/dev/pts/6) leaked on pvs invocation. Parent PID 8173: /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) : yes PVS support : no Mizar support : no Other provers support : at run-time (use why-config to configure) ... Error: The file /usr/local/lib/coq/user-contrib/Float/AllFloat.vo contains library AllFloat and not library Float.AllFloat make: *** [lib/coq/WhyFloatsStrictLegacy.vo] Error 1 [@@THALES GROUP RESTRICTED@@] -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120725/fc610cce/attachment-0001.html>