Improved replaying

examples/nightly-bench.sh

@@ -4,8 +4,8 @@ OUT=$PWD/nightly-bench.out
 REPORT=$PWD/nightly-bench.report
 
 notify() {
-    mail -s "Why3 nightly bench" why3-commits@lists.gforge.inria.fr < $REPORT
-    # cat $REPORT
+    # mail -s "Why3 nightly bench" why3-commits@lists.gforge.inria.fr < $REPORT
+    cat $REPORT
     exit 0
 }
 
@@ -43,6 +43,9 @@ else
     echo "Prover detection succeeded. " >> $REPORT
 fi
 
+# increase number of cores used
+perl -pi -e 's/running_provers_max = 2/running_provers_max = 4/' why.conf
+
 # do we want to do "make bench" ?
 
 # replay proofs

src/ide/replay.ml

@@ -158,7 +158,8 @@ let init =
 	  p.Session.prover_name ^ " " ^ p.Session.prover_version
         | M.Transformation tr -> Session.transformation_id tr.M.transf
     in
-    eprintf "Item '%s' loaded@." name
+    (* eprintf "Item '%s' loaded@." name *)
+    ()
 
 let string_of_result result =
   match result with

src/ide/session.ml

@@ -1334,8 +1334,9 @@ let check_external_proof g a =
         | Scheduled | Running -> ()
         | Undone -> assert false
         | InternalFailure msg ->
-            Format.printf "goal '%s', prover '%s': internal failure '%a'@."
-              g.goal_name p.prover_id Exn_printer.exn_printer 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
         | Done new_res ->
@@ -1346,16 +1347,16 @@ let check_external_proof g a =
                     begin
                       check_failed := true;
                       Format.printf
-                        "goal '%s', prover '%s': %a instead of %a@."
-                        g.goal_name p.prover_id 
+                        "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': no former result available@."
-                    g.goal_name p.prover_id
+                    "goal '%s', prover '%s %s': no former result available@."
+                    g.goal_name p.prover_name p.prover_version
     in
     let old = if a.edited_as = "" then None else
       begin