Hello;
I'm a new user of why3 prover; I want to try his installation but I
always have the 'ide' is not a Why3 command problem.
my configuration is as follows:
root@sara-HP-Pavilion-dv7-Notebook-PC:/home/sara# opam list
[WARNING] Running as root is not recommended
# Installed packages for system:
alt-ergo 2.2.0 Alt-Ergo, an SMT Solver for Software
Verification
base-bigarray base Bigarray library distributed with the
OCaml compil
base-threads base Threads library distributed with the OCaml
compile
base-unix base Unix library distributed with the OCaml
compiler
camlzip 1.07 Provides easy access to compressed files
in ZIP, G
conf-autoconf 0.1 Virtual package relying on autoconf
installation.
conf-gmp 1 Virtual package relying on a GMP lib
system instal
conf-gtksourceview 2 Virtual package relying on a GtkSourceView
system
conf-m4 1 Virtual package relying on m4
conf-perl 1 Virtual package relying on perl
conf-pkg-config 1.1 Virtual package relying on pkg-config
installation
conf-which 1 Virtual package relying on which
lablgtk 2.18.6 OCaml interface to GTK+
menhir 20180530 LR(1) parser generator
num 1.1 The legacy Num library for
arbitrary-precision int
ocamlbuild 0.12.0 OCamlbuild is a build system with builtin
rules to
ocamlfind 1.8.0 A library manager for OCaml
ocplib-simplex 0.4 A library implementing a simplex
algorithm, in a f
psmt2-frontend 0.1 A library to parse and type-check a
conservative e
why3 1.0.0 Why3 environment for deductive program
verificatio
zarith 1.7 Implements arithmetic and logical
operations over
root@sara-HP-Pavilion-dv7-Notebook-PC:/home/sara# why3 config --detect
root@sara-HP-Pavilion-dv7-Notebook-PC:/home/sara# why3 config --detect
Found prover CVC3 version 2.4.1, OK.
Found prover Z3 version 4.4.1 (old version, please consider upgrading).
Found prover Z3 version 4.4.1 (old version, please consider upgrading).
Found prover Z3 version 4.4.1 (old version, please consider upgrading).
Found prover Coq version 8.6, but no Why3 libraries were compiled for it
warning: Prover Alt-Ergo version 2.2.0 is not known to be supported.
Known versions for this prover: 2.0.0
Known old versions for this prover: 1.01, 1.30
5 prover(s) added (including 1 prover(s) with an unrecognized version)
Generating strategies:
Prover Z3 4.4.1 will be used in Auto level >= 1
== Found /root/.opam/system/lib/why3/plugins/dimacs.cmxs ==
== Found /root/.opam/system/lib/why3/plugins/python.cmxs ==
== Found /root/.opam/system/lib/why3/plugins/genequlin.cmxs ==
== Found /root/.opam/system/lib/why3/plugins/tptp.cmxs ==
Save config to /root/.why3.conf
root@sara-HP-Pavilion-dv7-Notebook-PC:/home/sara# cd whyproject/
root@sara-HP-Pavilion-dv7-Notebook-PC:/home/sara/whyproject# ls
BPMNGraph.mlw BPMNTypes BPMNTypes.mlw closestpair.mlw CodeAll.mlw
root@sara-HP-Pavilion-dv7-Notebook-PC:/home/sara/whyproject# why3 ide
BPMNTypes
'ide' is not a Why3 command.
Available commands:
config
doc
execute
extract
prove
realize
replay
session
shell
wc
webserver
how can I fix that ?
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
