Replayer: more detailed statistics

Version

 # Why version
-VERSION=0.64
+VERSION=0.70alpha
 

examples/regtests.sh

@@ -15,7 +15,7 @@ run_dir () {
         ../bin/why3replayer.opt $d 2> $TMPERR > $TMP
         ret=$?
 	if test "$ret" != "0"  ; then
-	    echo "FAILED (ret code=$ret):"
+	    echo -n "FAILED (ret code=$ret):"
             out=`head -1 $TMP`
             if test -z "$out" ; then
                echo "standard error: (standard output empty)"
@@ -25,7 +25,8 @@ run_dir () {
             fi
 	    res=1
 	else
-	    echo "OK"
+	    echo -n "OK"
+	    cat $TMP
 	fi
     done
 }

src/ide/replay.ml

@@ -6,6 +6,7 @@ open Why
 let includes = ref []
 let file = ref None
 let opt_version = ref false
+let opt_stats = ref true
 
 let spec = Arg.align [
   ("-I",
@@ -16,6 +17,9 @@ let spec = Arg.align [
    Arg.String (fun s -> input_files := s :: !input_files),
    "<f> add file f to the project (ignored if it is already there)") ;
 *)
+  ("-s",
+   Arg.Clear opt_stats,
+   " do not print statistics") ;
   ("-v",
    Arg.Set opt_version,
    " print version information") ;
@@ -52,7 +56,7 @@ let fname = match !file with
 let config = Whyconf.read_config None
 
 let loadpath = (Whyconf.loadpath (Whyconf.get_main config))
-  (* @ List.rev !includes *)
+  @ List.rev !includes 
 
 let env = Lexer.create_env loadpath
 
@@ -231,16 +235,75 @@ let project_dir =
   else
     failwith "file does not exist"
 
-let main () =
+let goal_statistics (goals,n,m) g =
+  if M.goal_proved g then (goals,n+1,m+1) else (g::goals,n,m+1)
+
+let theory_statistics (ths,n,m) th =
+  let goals,n1,m1 = List.fold_left goal_statistics ([],0,0) (M.goals th) in
+  ((th,goals,n1,m1)::ths,(if M.verified th then n+1 else n),m+1)
+
+let file_statistics (files,n,m) f =
+  let ths,n1,m1 = List.fold_left theory_statistics ([],0,0) f.M.theories in
+  ((f,ths,n1,m1)::files,(if f.M.file_verified then n+1 else n),m+1)
+
+let print_statistics files =
+  List.iter 
+    (fun (f,ths,n,m) ->
+       if n<m then
+	 begin
+	   printf "   +--file %s: %d/%d@." f.M.file_name n m;
+	   List.iter 
+	     (fun (th,goals,n,m) ->
+		if n<m then
+		  begin
+		    printf "      +--theory %s: %d/%d@." 
+		      (M.theory_name th) n m;
+		    List.iter 
+		      (fun g ->
+			 printf "         +--goal %s not proved@." (M.goal_name g)) 
+		      (List.rev goals)
+		  end)
+	     (List.rev ths)
+	 end)
+    (List.rev files)
+      
+let print_report (g,p,r) = 
+  printf "   goal '%s', prover '%s': " g p;
+  match r with
+  | M.Wrong_result(new_res,old_res) -> 
+      printf "%a instead of %a@."
+        Call_provers.print_prover_result new_res 
+        Call_provers.print_prover_result old_res
+  | M.No_former_result ->
+      printf "no former result available@."
+  | M.CallFailed msg ->
+      printf "internal failure '%a'@." Exn_printer.exn_printer msg;
+  | M.Prover_not_installed ->
+      printf "not installed@."
+
+	
+
+let () =
   try
     eprintf "Opening session...@?";
     M.open_session ~env ~config ~init ~notify project_dir;
     M.maximum_running_proofs :=
       Whyconf.running_provers_max (Whyconf.get_main config);
     eprintf " done@.";
-    let callback b =
-      if b then (eprintf "Check failed.@."; exit 1) 
-      else (eprintf "Everything OK.@.";exit 0)
+    let callback report =
+      let files,n,m = 
+	List.fold_left file_statistics ([],0,0) (M.get_all_files ()) 
+      in
+      printf " %d/%d@." n m ;
+      match report with
+	| [] -> 
+	    eprintf "Everything OK.@.";
+	    exit 0
+	| _ ->
+	    List.iter print_report report;
+	    if !opt_stats && n<m then print_statistics files;
+	    eprintf "Check failed.@."; 
+	    exit 1 
     in
     M.check_all ~callback;
     try main_loop ()
@@ -252,4 +315,8 @@ let main () =
     exit 1
 
 
-let () = main ()
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. bin/why3replayer.byte"
+End:
+*)

src/ide/session.ml

@@ -1356,7 +1356,17 @@ let replay ~obsolete_only ~context_unproved_goals_only a =
 (* method: check existing proofs *)
 (*********************************)
 
-let check_failed = ref false
+type report =
+  | Wrong_result of Call_provers.prover_result * Call_provers.prover_result  
+  | CallFailed of exn
+  | Prover_not_installed 
+  | No_former_result 
+
+let reports = ref []
+
+let push_report g p r =
+  reports := (g.goal_name,p,r) :: !reports
+
 let proofs_to_do = ref 0
 let proofs_done = ref 0
 
@@ -1378,43 +1388,33 @@ let check_external_proof g a =
   if running then ()
   else
     begin
-    incr proofs_to_do;
+      incr proofs_to_do;
       match a.prover with
         | Undetected_prover s ->
-            Format.printf "goal '%s', prover '%s': not installed@."
-              g.goal_name s;
-            check_failed := true;
-            incr proofs_done
+	    push_report g s Prover_not_installed;
+            incr proofs_done;
+	    set_proof_state ~obsolete:false a Undone
         | Detected_prover p ->
+	    let p_name = p.prover_name ^ " " ^ p.prover_version in
             let callback result =
               match result with
                 | Scheduled | Running -> ()
                 | Undone -> assert false
                 | InternalFailure msg ->
-                    Format.printf 
-                      "goal '%s', prover '%s %s': internal failure '%a'@."
-                      g.goal_name p.prover_name p.prover_version
-                      Exn_printer.exn_printer msg;
-                    check_failed := true;
-                    incr proofs_done
+		    push_report g p_name (CallFailed msg);
+                    incr proofs_done;
+		    set_proof_state ~obsolete:false a result
                 | Done new_res ->
+                    begin
+		      match a.proof_state with
+			| Done old_res ->
+                            if same_result old_res new_res then () else
+			      push_report g p_name (Wrong_result(new_res,old_res))
+			| _ ->
+			    push_report g p_name No_former_result
+		    end;
                     incr proofs_done;
-                    match a.proof_state with
-                      | Done old_res ->
-                        if same_result old_res new_res then () else
-                          begin
-                            check_failed := true;
-                            Format.printf
-                              "goal '%s', prover '%s %s': %a instead of %a@."
-                              g.goal_name p.prover_name p.prover_version
-                              Call_provers.print_prover_result new_res 
-                              Call_provers.print_prover_result old_res
-                          end
-                    | _ ->
-                        check_failed := true;
-                        Format.printf
-                          "goal '%s', prover '%s %s': no former result available@."
-                          g.goal_name p.prover_name p.prover_version
+		    set_proof_state ~obsolete:false a result
           in
           let old = if a.edited_as = "" then None else
             begin
@@ -1438,7 +1438,7 @@ let rec check_goal_and_children g =
     g.transformations
 
 let check_all ~callback =
-  check_failed := false;
+  reports := [];
   proofs_to_do := 0;
   proofs_done := 0;
   List.iter
@@ -1453,7 +1453,7 @@ let check_all ~callback =
       begin
 	Printf.eprintf "\n%!";
 	decr maximum_running_proofs;
-        callback !check_failed; 
+        callback !reports; 
         false
       end
     else true

src/ide/session.mli

@@ -240,11 +240,18 @@ module Make(O: OBSERVER) : sig
         with result was 'valid'
     *)
 
-  val check_all: callback:(bool -> unit) -> unit
+  type report =
+    | Wrong_result of Call_provers.prover_result * Call_provers.prover_result  
+    | CallFailed of exn
+    | Prover_not_installed 
+    | No_former_result 
+
+  val check_all: callback:((string * string * report) list -> unit) -> unit
     (** [check_all ()] reruns all the proofs of the session, and reports
         all difference with the current state 
         (does not change the session state)
-        When finished, calls the callback with argument true if there is at least one difference, false otherwise
+        When finished, calls the callback with the list of failed comparisons,
+	which are triples (goal name, prover, report)
     *)
 
   val reload_all: unit -> unit