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>