Improved statistics

doc/library.tex

@@ -4,7 +4,9 @@
 We provide here a short description of logic symbols defined in the
 standard library. Only the most general-purpose ones are
 described. For more details, one should directly read the
-corresponding file, or alternatively, use the \verb|why3| with option
+corresponding file, 
+\todo{Plutot la version produite avec why3doc}
+or alternatively, use the \verb|why3| with option
 \verb|-T| and a qualified theory name, for example:
 \begin{verbatim}
 > why3 -T bool.Ite
@@ -37,6 +39,8 @@ defined in it.
 
 \section{Library \texttt{int}}
 
+\todo{Completer}
+
 \begin{description}
 
 \item[Int] basic operations \verb|+|, \verb|-| and \verb|*|; comparison
@@ -79,7 +83,9 @@ defined in it.
 
 \item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|.
 
-\item[Power] function \verb|pow| with two real parameters.
+\item[PowerReal] function \verb|pow| with two real parameters.
+
+\item[PowerInt] function \verb|pow| with integer only exponents.
 
 \item[Trigonometry] functions \verb|cos|, \verb|sin|, \verb|tan|, and
   \verb|atan|. Constant \verb|pi|.
@@ -111,6 +117,8 @@ is inspired by~\cite{ayad10ijcar}.
 
 \section{Library \texttt{array}}
 
+\todo{Mettre a jour}
+
 \begin{description}
 
 \item[Array] polymorphic arrays, a.k.a maps. Type \verb|t|
@@ -213,6 +221,8 @@ is inspired by~\cite{ayad10ijcar}.
 
 \section{Library \texttt{string}}
 
+\todo{Detailler}
+
 \begin{description}
 \item[Char]
 \item[String]

doc/manpages.tex

@@ -4,6 +4,9 @@
 \section{Compilation, Installation}
 \label{sec:install}
 
+\todo{Cette section pourrait etre un chapitre a part du reference
+  manual}
+
 Compilation of \why must start with a configuration phase which is run as
 \begin{verbatim}
 ./configure
@@ -270,7 +273,23 @@ the actions of the various menus and buttons of the interface.
 \item[-I] $d$: adds $d$ in the load path, to search for theories.
 \end{description}
 
-\todo{option -extra-config and others}
+\todo{option -extra-config and others:}
+
+\begin{verbatim}
+  -L <s>                add s to loadpath
+  --library             same as -L
+  -I                    same as -L (obsolete)
+  -C <file>             Read configuration from <file>
+  --config              same as -C
+  --extra-config <file> Read additional configuration from <file>
+  --list-debug-flags    List known debug flags
+  --debug-all           Set all debug flags (except flags which change the behavior)
+  --debug <flag>        Set a debug flag
+  -v                    print version information
+\end{verbatim}
+
+\todo{Si ces options sont generales a toutes les commandes, il
+  faudrait les mettre dans une section preliminaire a ce chapitre}
 
 \subsection{Left toolbar actions}
 
@@ -370,6 +389,9 @@ The preferences window allows you customize
 
 \subsection{Structure of the database file}
 
+\todo{Cette subsection n'est pas specifique a l'IDE, devrait etre a
+  part, voire en annexe}
+
 The session state is stored in an XML file named
 \texttt{\textsl{<dir>}/why3session.xml}, where \texttt{\textsl{<dir>}}
 is the directory of the project.
@@ -581,38 +603,30 @@ All the commands above share the following common set of options:
 common options:
 \begin{description}
 \item[\texttt{-C <file>}] reads configuration from \texttt{file}
-\item[\texttt{--config}]  same as \texttt{-C}
-\item[\texttt{--extra-config <file>}] reads additional configuration from \texttt{<file>}
+\item[\texttt{-{}-config}]  same as \texttt{-C}
+\item[\texttt{-{}-extra-config <file>}] reads additional configuration from \texttt{<file>}
 \item[\texttt{-L <dir>}]              adds \texttt{<dir>} to the library search path
-\item[\texttt{--library}]             same as \texttt{-L}
+\item[\texttt{-{}-library}]             same as \texttt{-L}
 \item[\texttt{-v}]                    prints version information
-\item[\texttt{--list-debug-flags}]    lists known debug flags
-\item[\texttt{--debug-all}]           sets all debug flags (except flags which change the behavior)
-\item[\texttt{--debug <flag>}]        sets a debug flag
+\item[\texttt{-{}-list-debug-flags}]    lists known debug flags
+\item[\texttt{-{}-debug-all}]           sets all debug flags (except flags which change the behavior)
+\item[\texttt{-{}-debug <flag>}]        sets a debug flag
 \end{description}
 
 \subsection{Command \texttt{info}}
 
-\texttt{why3session info} reports informations:
-\begin{itemize}
-\item Option \verb|--provers| prints the provers that appear inside
+The command \texttt{why3session info} reports various informations
+about the session, depending on the following specific options.
+\begin{description}
+\item[\texttt{-{}-provers}] prints the provers that appear inside
   the session, one by line.
-\item Option \verb|--edited-files| prints all the files that appear in
+\item[\texttt{-{}-edited-files}] prints all the files that appear in
   the session as edited proofs.
-\item Option \verb|--stats| prints various proofs statistics, as
+\item[\texttt{-{}-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
-  be verified if the proof result is \verb|valid| and the proof is not
-  obsolete. However here specially we separate these two
-  properties. On the one hand if the proof suffers from an internal
-  failure we mark it with an exclamation mark \verb|!|, otherwise if
-  it is not valid we mark it with a question mark \verb|?|, finally if
-  it is valid we add nothing. On the other hand if the proof is
-  obsolete we mark it with an \verb|O| and if it is archived we mark
-  it with an \verb|A|.
-\item Option \verb|--print0| separates the results of the options
+\item[\texttt{-{}-tree}] prints the structure of the session as a
+  tree in ASCII, as detailed below.
+\item[\texttt{-{}-print0}] separates the results of the options
   \verb|provers| and \verb|--edited-files| by the character number 0
   instead of end of line \verb|\n|. That allows you to safely use
   (even if the filename contains space or carriage return) the result
@@ -628,7 +642,22 @@ why3session info --edited-files --print0 vstte12_bfs.mlw | \
     xargs -0 git add
 \end{verbatim}
 
-\end{itemize}
+\end{description}
+
+\paragraph{Session Tree}
+
+The hierarchical structure of the session is printed as a tree in
+ASCII. The files, theories, goals are marked with a question mark
+\verb|?|, if they are not verified. A proof is usually said to be
+verified if the proof result is \verb|valid| and the proof is not
+obsolete. However here specially we separate these two properties. On
+the one hand if the proof suffers from an internal failure we mark it
+with an exclamation mark \verb|!|, otherwise if it is not valid we
+mark it with a question mark \verb|?|, finally if it is valid we add
+nothing. On the other hand if the proof is obsolete we mark it with an
+\verb|O| and if it is archived we mark it with an \verb|A|.
+
+\todo{Example}
 
 \paragraph{Session Statistics}
 
@@ -637,20 +666,20 @@ The proof statistics given by option \verb|--stats| are as follows:
 \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
+  proved by any prover, even after a transformation.
+\item Goals proved by only one prover: the goals for which there is 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
+\item Statistics 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}.
+  sub-goals generated by transformations. The respective minimum,
+  maximum and average time and on average running time is
+  shown. Beware that these time data are computed on the
+  goals \emph{where the prover was successfull}.
 \end{itemize}
 
+\todo{Example}
 
 \subsection{Command \texttt{latex}}
 
@@ -669,20 +698,19 @@ The specific options are
 \end{description}
 
 
-
 \paragraph{Customizing LaTeX output}
 
 The generated LaTeX files contain some macros that must be defined
 externally.  Various definitions can be given to them to customize the
 output.
-\begin{itemize}
-\item \verb|\provername|: macro with one parameter, a prover name
-\item \verb|\valid|: macro with one parameter, used where the corresponding prover answers that the goal is valid. The parameter is the time in seconds.
-\item \verb|\noresult|: macro without parameter, used where no result
+\begin{description}
+\item[\texttt{\bs{}provername}]: macro with one parameter, a prover name
+\item[\texttt{\bs{}valid}]: macro with one parameter, used where the corresponding prover answers that the goal is valid. The parameter is the time in seconds.
+\item[\texttt{\bs{}noresult}]: macro without parameter, used where no result
   exists for the corresponding prover
-\item \verb|\timeout|: macro without parameter, used where the corresponding prover reached the time limit
-\item \verb|\explanation|: macro with one parameter, the goal name or its explanation
-\end{itemize}
+\item[\texttt{\bs{}timeout}]: macro without parameter, used where the corresponding prover reached the time limit
+\item[\texttt{\bs{}explanation}]: macro with one parameter, the goal name or its explanation
+\end{description}
 
 \begin{figure}[t]
   \begin{center}
@@ -727,24 +755,24 @@ Specific options for this command are as follows.
 \item[\texttt{-o}] 
 the directory to output the produces files ('-' for stdout)
 
-\item[\texttt{--context}] adds context around the generated code in
+\item[\texttt{-{}-context}] adds context around the generated code in
   order to allow direct visualisation (header, css, ...). It also adds
   in the directory all the needed external files. It can't be set with
   stdout output.
 
-\item[\texttt{--style <s>}] sets the style to
+\item[\texttt{-{}-style <s>}] sets the style to
   use, among \texttt{simpletree}, \texttt{jstree} and \texttt{table}, defaults to \texttt{table}.
 
-\item[\texttt{--add\_pp <suffix> <cmd> <out\_suffix>}] adds for the
+\item[\texttt{-{}-add\_pp <suffix> <cmd> <out\_suffix>}] adds for the
   given prefix the given pretty-printer, the new file as the given
   out\_suffix. cmd must contain
   '\%i' which will be replaced by the input file
                          and '\%o' which will be replaced by the
                          output file.
 
-\item[\texttt{--coqdoc}] use the coqdoc command to display Coq proof
-  scripts. This is equivalent to \texttt{--add\_pp .v "coqdoc
-    --no-index --html -o \%o \%i" .html}
+\item[\texttt{-{}-coqdoc}] use the coqdoc command to display Coq proof
+  scripts. This is equivalent to \texttt{-{}-add\_pp .v "coqdoc
+    -{}-no-index -{}-html -o \%o \%i" .html}
 
 \end{description}
  

doc/manual.tex

@@ -2,6 +2,9 @@
 
 % rubber: module index
 
+% tells memoir style to number subsections
+\setsecnumdepth{subsection}
+
 \usepackage[T1]{fontenc}
 \usepackage{lmodern}
 %\usepackage{url}

src/why3session/why3session_info.ml

@@ -61,7 +61,7 @@ type proof_stats =
       prover_avg_time : float Hprover.t;
       prover_max_time : float Hprover.t;
       prover_num_proofs : int Hprover.t;
-      prover_data : (string) Hprover.t
+      (* prover_data : (string) Hprover.t *)
     }
 
 let new_proof_stats () =
@@ -73,7 +73,7 @@ let new_proof_stats () =
     prover_avg_time = Hprover.create 3;
     prover_max_time = Hprover.create 3;
     prover_num_proofs =  Hprover.create 3;
-    prover_data = Hprover.create 3 }
+    (* prover_data = Hprover.create 3  *)}
 
 let apply_f_on_hashtbl_entry ~tbl ~f ~name  =
   try
@@ -172,12 +172,117 @@ let stats_of_file stats _ file =
   let theories = file.file_theories in
   List.iter (stats_of_theory file stats) theories
 
+
+
+type 'a goal_stat =
+  | No of ('a transf * ('a goal * 'a goal_stat) list) list
+  | Yes of (prover * float) list * ('a transf * ('a goal * 'a goal_stat) list) list
+
+let rec stats2_of_goal ~nb_proofs g : notask goal_stat = 
+  let proof_list =
+    PHprover.fold
+      (fun prover proof_attempt acc ->
+        match proof_attempt.proof_state with
+          | Done result ->
+            begin
+              match result.Call_provers.pr_answer with
+                | Call_provers.Valid ->
+                  (prover, result.Call_provers.pr_time) :: acc
+                | _ ->
+                  acc
+            end
+          | _ -> acc)
+      g.goal_external_proofs
+      []
+  in
+  let l =
+    PHstr.fold
+      (fun _ tr acc ->
+        match stats2_of_transf ~nb_proofs tr with
+          | [] -> acc
+          | r -> (tr,List.rev r)::acc)
+      g.goal_transformations
+      []
+  in
+  if match nb_proofs with
+    | 0 -> not g.goal_verified
+    | 1 -> List.length proof_list = 1
+    | _ -> assert false
+      then Yes(proof_list,l) else No(l)
+
+and stats2_of_transf ~nb_proofs tr : (notask goal * notask goal_stat) list =
+  List.fold_left
+    (fun acc g ->
+      match stats2_of_goal ~nb_proofs g with
+        | No [] -> acc
+        | r -> (g,r)::acc)
+    [] tr.transf_goals
+
+let print_res fmt (p,t) = fprintf fmt "%a (%.2f)" print_prover p t
+
+let rec print_goal_stats depth (g,l) = 
+  for i=1 to depth do printf "  " done;
+  printf "+-- goal %s" g.goal_name.Ident.id_string;
+  match l with
+    | No l ->
+      printf "@\n";
+      List.iter (print_transf_stats (depth+1)) l
+    | Yes(pl,l) ->
+      begin
+        match pl with
+          | [] -> printf "@\n"
+          | _ -> printf ": %a@\n" (Pp.print_list pp_print_space print_res) pl
+      end;
+      List.iter (print_transf_stats (depth+1)) l
+
+and print_transf_stats depth (tr,l) =
+  for i=1 to depth do printf "  " done;
+  printf "+-- transformation %s@\n" tr.transf_name;
+  List.iter (print_goal_stats (depth+1)) l
+
+let stats2_of_theory ~nb_proofs th =
+  List.fold_left
+    (fun acc g ->
+      match stats2_of_goal ~nb_proofs g with
+        | No [] -> acc
+        | r -> (g,r)::acc)
+    [] th.theory_goals
+
+let print_theory_stats (th,r) =
+  printf "  +-- theory %s@\n" th.theory_name.Ident.id_string;
+  List.iter (print_goal_stats 2) r
+
+let stats2_of_file ~nb_proofs file =
+  List.fold_left
+    (fun acc th ->
+      match stats2_of_theory ~nb_proofs th with
+        | [] -> acc
+        | r -> (th,List.rev r)::acc)
+    [] file.file_theories
+
+let stats2_of_session ~nb_proofs s =
+  PHstr.fold
+    (fun _ f acc ->
+      match stats2_of_file ~nb_proofs f with
+        | [] -> acc
+        | r -> (f,List.rev r)::acc)
+    s.session_files []
+
+let print_file_stats (f,r) =
+  printf "+-- file %s@\n" f.file_name;
+  List.iter print_theory_stats r
+
+let print_session_stats = List.iter print_file_stats
+
+
+(*
 let fill_prover_data stats session =
   Sprover.iter
     (fun prover ->
       Hprover.add stats.prover_data prover
-        (prover.prover_name ^ " " ^ prover.prover_version))
+        (string_of_prover prover))
     (get_used_provers session)
+*)
 
 let finalize_stats stats =
   Hprover.iter
@@ -187,42 +292,30 @@ let finalize_stats stats =
         (time /. (float_of_int n)))
     stats.prover_avg_time
 
-let print_stats stats =
+let print_stats r0 r1 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;
+  print_session_stats r0;
+  (* Sstr.iter (fun s -> printf "%s@\n" s) stats.no_proof; *)
   printf "@]@\n";
 
   printf "== Goals proved by only one prover ==@\n  @[";
-  Sstr.iter (fun s -> printf "%s@\n" s) stats.only_one_proof;
+  print_session_stats r1;
+  (* Sstr.iter (fun s -> printf "%s@\n" s) stats.only_one_proof; *)
   printf "@]@\n";
 
-  printf "== Number of proofs per prover ==@\n  @[";
-  Hprover.iter (fun prover n -> printf "%-10s: %d@\n"
-    (string_of_prover prover) n)
+  printf "== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==@\n  @[";
+  Hprover.iter (fun prover n -> printf "%-20s : %3d %6.2f %6.2f %6.2f@\n"
+    (string_of_prover prover) n
+    (Hprover.find stats.prover_min_time prover)
+    (Hprover.find stats.prover_max_time prover)
+    (Hprover.find stats.prover_avg_time prover))
     stats.prover_num_proofs;
-  printf "@]@\n";
-
-  printf "== Minimum time per prover ==@\n  @[";
-  Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
-    (string_of_prover prover) time)
-    stats.prover_min_time;
-  printf "@]@\n";
-
-  printf "== Maximum time per prover ==@\n  @[";
-  Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
-    (string_of_prover prover) time)
-    stats.prover_max_time;
-  printf "@]@\n";
-
-  printf "== Average time per prover ==@\n  @[";
-  Hprover.iter (fun prover time -> printf "%-10s : %.3f s@\n"
-    (string_of_prover prover) time)
-    stats.prover_avg_time;
   printf "@]@\n"
 
+
 let run_one fname =
   let project_dir = Session.get_project_dir fname in
   if !opt_project_dir then printf "%s@." project_dir;
@@ -243,10 +336,12 @@ let run_one fname =
   if !opt_stats_print then
     begin
       let stats = new_proof_stats () in
-      fill_prover_data stats session;
+      (* fill_prover_data stats session; *)
       PHstr.iter (stats_of_file stats) session.session_files;
+      let r0 = stats2_of_session ~nb_proofs:0 session in
+      let r1 = stats2_of_session ~nb_proofs:1 session in
       finalize_stats stats;
-      print_stats stats
+      print_stats r0 r1 stats;
     end