Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Plateform Why-2.31
- Subject: [Frama-c-discuss] Plateform Why-2.31
- From: mickael.dahan at thalesgroup.com (DAHAN Mickael)
- Date: Wed, 25 Jul 2012 17:31:59 +0200
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>