Commit c21cc7f7 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

a few improvement in the stats, and its documentation

parent 9b3951e0
......@@ -147,14 +147,14 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
- (CLAUDE) revoir documentation du smoke detector
- Documenter l'utilisation de plusieurs versions du meme prouveur comme CVC3 et Z3
DONE, mais reorganiser la section, lien sur la page web des prouveurs
- DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable
mais remplacer le ":" par " " (Arg.Tuple)
- (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé. Et les mettre au point:
. Lors d'un replay, le dialogue "replace proof" apparait un nombre important de fois,
il faut absolument pouvoir interrompre, ou donner une reponse qui soit appliquée pour le reste.
(le 3e bouton "never replace..." ne semble pas jourer ce role...)
. le dialogue "replace proof" est de toute facon trop large, et les choix possibles sont confus.
- DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable
mais remplacer le ":" par " " (Arg.Tuple)
- (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et "timelimit"
DONE, en fait c'était déjà le cas
- (WHO?) complete api.tex: explain how to build theories, apply
......
......@@ -95,12 +95,12 @@ The \why executables are then available in the subdirectory \texttt{bin/}.
\label{sec:installlib}
By default, the \why library is not installed. It can be installed using
\begin{verbatim}
make byte opt
make install_lib
\end{verbatim}
\begin{flushleft}\ttfamily
make byte opt \\
make install\_lib \mbox{\rmfamily (as super-user)}
\end{flushleft}
\section{Installation of external provers}
\subsection{Installation of external provers}
\label{provers}
\why can use a wide range of external theorem provers. These need to
......@@ -108,12 +108,28 @@ be installed separately, and then \why needs to be configured to use
them. There is no need to install these provers before compiling and
installing Why.
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
For installation of external provers, please refer to the specific
section about provers on the Web page \url{http://why3.lri.fr/}.
For configuring \why to use the provers, follow instructions given in
Section~\ref{sec:why3config}.
% The provers which are typically looked for are
% \begin{itemize}
% \item Alt-Ergo~\cite{conchon08smt,ergo}: \url{http://alt-ergo.lri.fr}
% \item CVC3~\cite{BarTin-CAV-07}: \url{http://cs.nyu.edu/acsys/cvc3/}
% \item Coq~\cite{CoqArt}: \url{http://coq.inria.fr}
% \item Eprover~\cite{schulz04ijcar}: \url{http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html}
% \item Gappa~\cite{melquiond08rnc}: \url{http://gappa.gforge.inria.fr/}
% \item Simplify~\cite{simplify05}: \url{http://secure.ucd.ie/products/opensource/Simplify/}
% \item Spass: \url{http://www.spass-prover.org/}
% \item Vampire: \url{http://www.voronkov.com/vampire.cgi}
% \item VeriT: \url{http://www.verit-solver.org/}
% \item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}, only versions 1.xx since versions 2.xx do not support quantifiers
% \item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
% \end{itemize}
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}
......@@ -143,21 +159,6 @@ is also human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, \eg{} different
versions of the same prover, or with different options.
The provers which are typically looked for are
\begin{itemize}
\item Alt-Ergo~\cite{conchon08smt,ergo}: \url{http://alt-ergo.lri.fr}
\item CVC3~\cite{BarTin-CAV-07}: \url{http://cs.nyu.edu/acsys/cvc3/}
\item Coq~\cite{CoqArt}: \url{http://coq.inria.fr}
\item Eprover~\cite{schulz04ijcar}: \url{http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html}
\item Gappa~\cite{melquiond08rnc}: \url{http://gappa.gforge.inria.fr/}
\item Simplify~\cite{simplify05}: \url{http://secure.ucd.ie/products/opensource/Simplify/}
\item Spass: \url{http://www.spass-prover.org/}
\item Vampire: \url{http://www.voronkov.com/vampire.cgi}
\item VeriT: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}, only versions 1.xx since versions 2.xx do not support quantifiers
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
\end{itemize}
\texttt{why3config} also detects the plugins installed in the \why
plugins directory (\eg{} \texttt{/usr/local/lib/why3/plugins}). A
plugin must register itself as a parser, a transformation or a
......@@ -598,6 +599,8 @@ common options:
the session, one by line.
\item Option \verb|--edited-files| prints all the files that appear in
the session as edited proofs.
\item Option \verb|--stats| prints various proofs statistics, as
detailed below.
\item Option \verb|--tree| prints the structure of the session as an
ASCII tree. The files, theories, goals are marked with a question
mark \verb|?|, if they are not verified. A proof is usually said to
......@@ -629,7 +632,25 @@ why3session info --edited-files --print0 vstte12_bfs.mlw | \
\paragraph{Session Statistics}
\todo{DETAILLER why3session info --stats}
The proof statistics given by option \verb|--stats| are as follows:
\begin{itemize}
\item Number of goals: give both the total number of goals, and the
number of those that are proved (possibly after a transformation).
\item Goals not proved: list of goals of the session which are not
proved by any prover, even after a transformtion.
\item Goals proved by only one prover: the goals for which there only
one successful proof. For each of these, the prover which was
successful is printed. This also includes the sub-goals generated by
transformations.
\item Number of proofs per prover: for each of the prover used in the
session, the number of proved goals is given. This also includes the
sub-goals generated by transformations.
\item Minimum/Maximum/Average time per prover: for each of the provers
used in the session, the respective minimal, maximal, and on average
running time is shown, for each of the goals \emph{where the prover
was successfull}.
\end{itemize}
\subsection{Command \texttt{latex}}
......
......@@ -2,24 +2,9 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter ignore: forall (a:Type), a -> unit.
Implicit Arguments ignore.
Parameter label_ : Type.
Parameter at1: forall (a:Type), a -> label_ -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter power: Z -> Z -> Z.
Require int.Int.
Parameter power: Z -> Z -> Z.
Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
......@@ -28,6 +13,7 @@ Axiom Power_s : forall (x:Z) (n:Z), (0%Z < n)%Z -> ((power x
Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
(* Why3 goal *)
Theorem Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
((0%Z <= m)%Z -> ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)
......@@ -35,6 +21,11 @@ intros x n m Hn Hm.
generalize Hm.
pattern m.
apply Z_lt_induction; auto.
(*
ae.
ca marche !!
*)
intros n0 Hind Hn0.
assert (h:(n0 = 0 \/ n0 > 0)%Z) by omega.
destruct h.
......@@ -46,6 +37,5 @@ rewrite (Power_s x n0).
ring.
omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -53,7 +53,9 @@ let spec =
type proof_stats =
{ mutable no_proof : Sstr.t;
{ mutable nb_goals : int;
mutable nb_proved_goals : int;
mutable no_proof : Sstr.t;
mutable only_one_proof : Sstr.t;
prover_min_time : float Hprover.t;
prover_avg_time : float Hprover.t;
......@@ -63,7 +65,9 @@ type proof_stats =
}
let new_proof_stats () =
{ no_proof = Sstr.empty;
{ nb_goals = 0;
nb_proved_goals = 0;
no_proof = Sstr.empty;
only_one_proof = Sstr.empty;
prover_min_time = Hprover.create 3;
prover_avg_time = Hprover.create 3;
......@@ -119,8 +123,7 @@ let update_perf_stats stats prover_and_time =
let string_of_prover p = Pp.string_of_wnl print_prover p
let rec stats_of_goal prefix_name stats goal =
let ext_proofs = goal.goal_external_proofs in
let proof_id = prefix_name ^ goal.goal_name.Ident.id_string in
stats.nb_goals <- stats.nb_goals + 1;
let proof_list =
PHprover.fold
(fun prover proof_attempt acc ->
......@@ -134,22 +137,26 @@ let rec stats_of_goal prefix_name stats goal =
acc
end
| _ -> acc)
ext_proofs
[] in
let no_transf = PHstr.length goal.goal_transformations = 0 in
begin match proof_list with
| [] when no_transf ->
stats.no_proof <- Sstr.add proof_id stats.no_proof
| [ (prover, time) ] when no_transf ->
stats.only_one_proof <-
Sstr.add
(proof_id ^ " : " ^ (string_of_prover prover))
stats.only_one_proof;
update_perf_stats stats (prover, time)
| _ ->
List.iter (update_perf_stats stats) proof_list end;
PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations
goal.goal_external_proofs
[]
in
List.iter (update_perf_stats stats) proof_list;
PHstr.iter (stats_of_transf prefix_name stats) goal.goal_transformations;
if not goal.goal_verified then
let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
stats.no_proof <- Sstr.add goal_name stats.no_proof
else
begin
stats.nb_proved_goals <- stats.nb_proved_goals + 1;
match proof_list with
| [ (prover, _) ] ->
let goal_name = prefix_name ^ goal.goal_name.Ident.id_string in
stats.only_one_proof <-
Sstr.add
(goal_name ^ " : " ^ (string_of_prover prover))
stats.only_one_proof
| _ -> ()
end
and stats_of_transf prefix_name stats _ transf =
let prefix_name = prefix_name ^ transf.transf_name ^ " / " in
......@@ -181,6 +188,9 @@ let finalize_stats stats =
stats.prover_avg_time
let print_stats stats =
printf "== Number of goals ==@\n total: %d proved: %d@\n@\n"
stats.nb_goals stats.nb_proved_goals;
printf "== Goals not proved ==@\n @[";
Sstr.iter (fun s -> printf "%s@\n" s) stats.no_proof;
printf "@]@\n";
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment