added initialization and cleanup of actions,
added option to suppress Isabelle output,
sledgehammer action produces its own report (no need for additional perl script)

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Sep 05 11:45:57 2009 +0200
@@ -12,8 +12,11 @@
   val setup : theory -> theory
 
   (* core *)
+  type init_action
+  type done_action
+  type run_action
   type action
-  val catch : string -> action -> action
+  val catch : (int -> string) -> run_action -> run_action
   val register : action -> theory -> theory
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     unit
@@ -47,12 +50,16 @@
 
 (* Mirabelle core *)
 
-type action = {pre: Proof.state, post: Toplevel.state option,
+
+type init_action = int -> theory -> theory
+type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
+type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
   timeout: Time.time, log: string -> unit} -> unit
+type action = init_action * run_action * done_action
 
 structure Actions = TheoryDataFun
 (
-  type T = action list
+  type T = (int * run_action * done_action) list
   val empty = []
   val copy = I
   val extend = I
@@ -63,11 +70,17 @@
 fun app_with f g x = (g x; ())
   handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
 
-fun catch tag f (st as {log, ...}) =
-  let fun log_exn e = log (tag ^ "exception:\n" ^ General.exnMessage e)
-  in app_with log_exn f st end
+fun catch tag f id (st as {log, ...}) =
+  let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
+  in app_with log_exn (f id) st end
 
-val register = Actions.map o cons
+fun register (init, run, done) thy =
+  let val id = length (Actions.get thy) + 1
+  in
+    thy
+    |> init id
+    |> Actions.map (cons (id, run, done))
+  end
 
 local
 
@@ -82,7 +95,7 @@
 fun apply_actions thy info (pre, post, time) actions =
   let
     fun apply f = f {pre=pre, post=post, timeout=time, log=log thy}
-    fun run f = (apply f; log_sep thy)
+    fun run (id, run, _) = (apply (run id); log_sep thy)
   in (log thy info; log_sep thy; List.app run actions) end
 
 fun in_range _ _ NONE = true
@@ -94,7 +107,7 @@
 
 in
 
-fun basic_hook tr pre post =
+fun run_actions tr pre post =
   let
     val thy = Proof.theory_of pre
     val pos = Toplevel.pos_of tr
@@ -108,6 +121,16 @@
     only_within_range thy pos (apply_actions thy info st) (Actions.get thy)
   end
 
+fun done_actions st =
+  let
+    val thy = Toplevel.theory_of st
+    val _ = log thy "\n\n";
+  in
+    thy
+    |> Actions.get
+    |> List.app (fn (id, _, done) => done id {last=st, log=log thy})
+  end
+
 end
 
 val whitelist = ["apply", "by", "proof"]
@@ -116,7 +139,9 @@
  (* FIXME: might require wrapping into "interruptible" *)
   if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
      member (op =) whitelist (Toplevel.name_of tr)
-  then basic_hook tr (Toplevel.proof_of pre) (SOME post)
+  then run_actions tr (Toplevel.proof_of pre) (SOME post)
+  else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post
+  then done_actions pre
   else ()   (* FIXME: add theory_hook here *)
 
 

--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sat Sep 05 11:45:57 2009 +0200
@@ -5,12 +5,17 @@
 structure Mirabelle_Arith : MIRABELLE_ACTION =
 struct
 
-fun arith_action {pre, timeout, log, ...} =
+fun arith_tag id = "#" ^ string_of_int id ^ " arith: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, timeout, log, ...} =
   if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
-  then log "arith: succeeded"
+  then log (arith_tag id ^ "succeeded")
   else ()
-  handle TimeLimit.TimeOut => log "arith: timeout"
+  handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
 
-fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
 
 end

--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat Sep 05 11:45:57 2009 +0200
@@ -5,7 +5,12 @@
 structure Mirabelle_Metis : MIRABELLE_ACTION =
 struct
 
-fun metis_action {pre, post, timeout, log} =
+fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, post, timeout, log} =
   let
     val thms = Mirabelle.theorems_of_sucessful_proof post
     val names = map Thm.get_name thms
@@ -16,12 +21,13 @@
     fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
   in
     (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
-    |> prefix "metis: "
+    |> prefix (metis_tag id)
     |> add_info
     |> log
   end
-  handle TimeLimit.TimeOut => log "metis: timeout"
+  handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
+       | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
 
-fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
 
 end

--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sat Sep 05 11:45:57 2009 +0200
@@ -5,18 +5,24 @@
 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
 struct
 
-fun quickcheck_action args {pre, timeout, log, ...} =
+fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run args id {pre, timeout, log, ...} =
   let
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
     val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
   in
     (case TimeLimit.timeLimit timeout quickcheck pre of
-      NONE => log "quickcheck: no counterexample"
-    | SOME _ => log "quickcheck: counterexample found")
+      NONE => log (qc_tag id ^ "no counterexample")
+    | SOME _ => log (qc_tag id ^ "counterexample found"))
   end
-  handle TimeLimit.TimeOut => log "quickcheck: timeout"
+  handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
+       | ERROR msg => log (qc_tag id ^ "error: " ^ msg)
 
 fun invoke args =
-  Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))
+  Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done)
 
 end

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 05 11:45:57 2009 +0200
@@ -5,6 +5,190 @@
 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
 struct
 
+val proverK = "prover"
+val keepK = "keep"
+val metisK = "metis"
+val full_typesK = "full_types"
+
+fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
+fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
+
+
+datatype data = Data of {
+  sh_calls: int,
+  sh_success: int,
+  sh_time: int,
+  metis_calls: int,
+  metis_success: int,
+  metis_time: int,
+  metis_timeout: int }
+
+fun make_data (sh_calls, sh_success, sh_time, metis_calls, metis_success,
+    metis_time, metis_timeout) =
+  Data {sh_calls=sh_calls, sh_success=sh_success, sh_time=sh_time,
+    metis_calls=metis_calls, metis_success=metis_success,
+    metis_time=metis_time, metis_timeout=metis_timeout}
+
+fun map_data f (Data {sh_calls, sh_success, sh_time, metis_calls,
+    metis_success, metis_time, metis_timeout}) =
+  make_data (f (sh_calls, sh_success, sh_time, metis_calls, metis_success,
+    metis_time, metis_timeout))
+
+val empty_data = make_data (0, 0, 0, 0, 0, 0, 0)
+
+val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+  metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success,
+  sh_time, metis_calls, metis_success, metis_time, metis_timeout))
+
+val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1,
+  sh_time, metis_calls, metis_success, metis_time, metis_timeout))
+
+fun inc_sh_time t = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+  sh_time + t, metis_calls, metis_success, metis_time, metis_timeout))
+
+val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+  metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+  sh_time, metis_calls + 1, metis_success, metis_time, metis_timeout))
+
+val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time,
+  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+  sh_success, sh_time, metis_calls, metis_success + 1, metis_time,
+  metis_timeout))
+
+fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time,
+  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+  sh_success, sh_time, metis_calls, metis_success, metis_time + t,
+  metis_timeout))
+
+val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time,
+  metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+  sh_success, sh_time, metis_calls, metis_success, metis_time,
+  metis_timeout + 1))
+
+
+local
+
+val str = string_of_int
+val str3 = Real.fmt (StringCvt.FIX (SOME 3))
+fun percentage a b = string_of_int (a * 100 div b)
+fun time t = Real.fromInt t / 1000.0
+fun avg_time t n =
+  if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
+
+fun log_sh_data log sh_calls sh_success sh_time =
+ (log ("Total number of sledgehammer calls: " ^ str sh_calls);
+  log ("Number of successful sledgehammer calls: " ^ str sh_success);
+  log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
+  log ("Total time for successful sledgehammer calls: " ^ str3 (time sh_time));
+  log ("Average time for successful sledgehammer calls: " ^
+    str3 (avg_time sh_time sh_success)))
+
+fun log_metis_data log sh_success metis_calls metis_success metis_time
+    metis_timeout =
+ (log ("Total number of metis calls: " ^ str metis_calls);
+  log ("Number of successful metis calls: " ^ str metis_success);
+  log ("Number of metis timeouts: " ^ str metis_timeout);
+  log ("Number of metis exceptions: " ^
+    str (sh_success - metis_success - metis_timeout));
+  log ("Success rate: " ^ percentage metis_success metis_calls ^ "%");
+  log ("Total time for successful metis calls: " ^ str3 (time metis_time));
+  log ("Average time for successful metis calls: " ^
+    str3 (avg_time metis_time metis_success)))
+
+in
+
+fun log_data id log (Data {sh_calls, sh_success, sh_time, metis_calls,
+    metis_success, metis_time, metis_timeout}) =
+  if sh_calls > 0
+  then
+   (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
+    log_sh_data log sh_calls sh_success sh_time;
+    log "";
+    if metis_calls > 0 then log_metis_data log sh_success metis_calls
+      metis_success metis_time metis_timeout else ())
+  else ()
+
+end
+
+
+(* Warning: we implicitly assume single-threaded execution here! *)
+val data = ref ([] : (int * data) list)
+
+fun init id thy = (change data (cons (id, empty_data)); thy)
+fun done id {log, ...} =
+  AList.lookup (op =) (!data) id
+  |> Option.map (log_data id log)
+  |> K ()
+
+fun change_data id f = (change data (AList.map_entry (op =) id f); ())
+
+
+local
+
+fun safe init done f x =
+  let
+    val y = init x
+    val z = Exn.capture f y
+    val _ = done y
+  in Exn.release z end
+
+fun init_sh NONE = !AtpWrapper.destdir
+  | init_sh (SOME path) =
+      let
+        (* Warning: we implicitly assume single-threaded execution here! *)
+        val old = !AtpWrapper.destdir
+        val _ = AtpWrapper.destdir := path
+      in old end
+
+fun done_sh path = AtpWrapper.destdir := path
+
+fun run_sh prover_name timeout st _ =
+  let
+    val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
+    val atp_timeout = AtpManager.get_timeout () 
+    val atp = prover atp_timeout NONE NONE prover_name 1
+    val ((success, (message, thm_names), time, _, _, _), time') =
+      TimeLimit.timeLimit timeout (Mirabelle.cpu_time atp) (Proof.get_goal st)
+  in
+    if success then (message, SOME (time + time', thm_names))
+    else (message, NONE)
+  end
+  handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
+       | TimeLimit.TimeOut => ("timeout", NONE)
+       | ERROR msg => ("error: " ^ msg, NONE)
+
+in
+
+fun run_sledgehammer args thm_names id {pre=st, timeout, log, ...} =
+  let
+    val _ = change_data id inc_sh_calls 
+    val prover_name =
+      AList.lookup (op =) args proverK
+      |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+    val dir = AList.lookup (op =) args keepK
+    val (msg, result) =
+      safe init_sh done_sh (run_sh prover_name timeout st) dir
+    val _ =
+      if is_some result
+      then
+        let
+          val time = fst (the result)
+          val _ = change_data id inc_sh_success
+          val _ = change_data id (inc_sh_time time)
+        in
+          log (sh_tag id ^ "succeeded (" ^ string_of_int time ^ ") [" ^
+            prover_name ^ "]:\n" ^ msg)
+        end
+      else log (sh_tag id ^ "failed: " ^ msg)
+  in change thm_names (K (Option.map snd result)) end
+
+end
+
+
+local
+
 fun thms_of_name ctxt name =
   let
     val lex = OuterKeyword.get_lexicons
@@ -18,100 +202,48 @@
     |> Source.exhaust
   end
 
-fun safe init done f x =
-  let
-    val y = init x
-    val z = Exn.capture f y
-    val _ = done y
-  in Exn.release z end
-
-val proverK = "prover"
-val keepK = "keep"
-val metisK = "metis"
-val full_typesK = "full_types"
-
-val sh_tag = "sledgehammer: "
-val metis_tag = "metis (sledgehammer): "
-
-
-local
-
-fun init NONE = !AtpWrapper.destdir
-  | init (SOME path) =
-      let
-        (* Warning: we implicitly assume single-threaded execution here! *)
-        val old = !AtpWrapper.destdir
-        val _ = AtpWrapper.destdir := path
-      in old end
-
-fun done path = AtpWrapper.destdir := path
-
-fun run prover_name timeout st _ =
-  let
-    val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
-    val atp_timeout = AtpManager.get_timeout () 
-    val atp = prover atp_timeout NONE NONE prover_name 1
-    val (success, (message, thm_names), time, _, _, _) =
-      TimeLimit.timeLimit timeout atp (Proof.get_goal st)
-  in if success then (message, SOME (time, thm_names)) else (message, NONE) end
-  handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
-       | TimeLimit.TimeOut => ("timeout", NONE)
-       | ERROR msg => ("error: " ^ msg, NONE)
-
 in
 
-fun run_sledgehammer args thm_names {pre=st, timeout, log, ...} =
+fun run_metis args thm_names id {pre=st, timeout, log, ...} =
   let
-    val prover_name =
-      AList.lookup (op =) args proverK
-      |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
-    val dir = AList.lookup (op =) args keepK
-    val (msg, result) = safe init done (run prover_name timeout st) dir
-    val _ =
-      if is_some result
-      then log (sh_tag ^ "succeeded (" ^ string_of_int (fst (the result)) ^
-        ") [" ^ prover_name ^ "]:\n" ^ msg)
-      else log (sh_tag ^ "failed: " ^ msg)
-  in change thm_names (K (Option.map snd result)) end
+    fun get_thms ctxt = maps (thms_of_name ctxt)
+
+    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
+    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
+
+    fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
+      | with_time (true, t) = (change_data id inc_metis_success;
+          change_data id (inc_metis_time t);
+          "succeeded (" ^ string_of_int t ^ ")")
+    fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
+      handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
+           | ERROR msg => "error: " ^ msg
+
+    val _ = log "-----"
+    val _ = change_data id inc_metis_calls
+  in
+    thm_names
+    |> get_thms (Proof.context_of st)
+    |> timed_metis
+    |> log o prefix (metis_tag id) 
+  end
 
 end
 
 
-fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
-  | with_time false t = "failed (" ^ string_of_int t ^ ")"
-
-fun run_metis args thm_names {pre=st, timeout, log, ...} =
-  let
-    fun get_thms ctxt = maps (thms_of_name ctxt)
-    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
-    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
-    fun timed_metis thms =
-      uncurry with_time (Mirabelle.cpu_time apply_metis thms)
-      handle TimeLimit.TimeOut => "timeout"
-           | ERROR msg => "error: " ^ msg
-    fun log_metis s = log (metis_tag ^ s)
-  in
-    if not (AList.defined (op =) args metisK) then ()
-    else if is_none (!thm_names) then ()
-    else
-      log "-----"
-      |> K (these (!thm_names))
-      |> get_thms (Proof.context_of st)
-      |> timed_metis
-      |> log_metis
-  end
-
-
-fun sledgehammer_action args (st as {log, ...}) =
+fun sledgehammer_action args id (st as {log, ...}) =
   let
     val thm_names = ref (NONE : string list option)
-    val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) st
-    val _ = Mirabelle.catch metis_tag (run_metis args thm_names) st
-  in () end
+    val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) id st
+  in
+    if AList.defined (op =) args metisK andalso is_some (!thm_names)
+    then Mirabelle.catch metis_tag (run_metis args (these (!thm_names))) id st
+    else ()
+  end
 
 fun invoke args =
   let
     val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
-  in Mirabelle.register (sledgehammer_action args) end
+  in Mirabelle.register (init, sledgehammer_action args, done) end
 
 end

--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Sat Sep 05 11:45:57 2009 +0200
@@ -26,6 +26,7 @@
   echo "    -T THEORY    parent theory to use (default $MIRABELLE_THEORY)"
   echo "    -O DIR       output directory for test data (default $out)"
   echo "    -t TIMEOUT   timeout for each action in seconds (default $timeout)"
+  echo "    -q           be quiet (suppress output of Isabelle process)" 
   echo
   echo "  Apply the given actions (i.e., automated proof tools)"
   echo "  at all proof steps in the given theory files."
@@ -46,7 +47,7 @@
 
 # options
 
-while getopts "L:T:O:t:?" OPT
+while getopts "L:T:O:t:q?" OPT
 do
   case "$OPT" in
     L)
@@ -61,15 +62,20 @@
     t)
       MIRABELLE_TIMEOUT="$OPTARG"
       ;;
+    q)
+      MIRABELLE_QUIET="true"
+      ;;
     \?)
       usage
       ;;
   esac
 done
 
+export MIRABELLE_QUIET
+
 shift $(($OPTIND - 1))
 
-ACTIONS="$1"
+export MIRABELLE_ACTIONS="$1"
 
 shift
 
@@ -83,6 +89,6 @@
 
 for FILE in "$@"
 do
-  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
+  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE"
 done
 

--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Sat Sep 05 11:45:57 2009 +0200
@@ -14,15 +14,15 @@
 my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
 my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
+my $be_quiet = $ENV{'MIRABELLE_QUIET'};
+my $actions = $ENV{'MIRABELLE_ACTIONS'};
 
 my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
 
 
 # arguments
 
-my $actions = $ARGV[0];
-
-my $thy_file = $ARGV[1];
+my $thy_file = $ARGV[0];
 my $start_line = "0";
 my $end_line = "~1";
 if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
@@ -122,15 +122,17 @@
 }
 close(LOG_FILE);
 
-my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
-
+my $quiet = "";
+if (defined $be_quiet and $be_quiet ne "") {
+  $quiet = " > /dev/null 2>&1";
+}
 
-# produce report
+print "Mirabelle: $thy_file\n" if ($quiet ne "");
 
-if ($result == 0) {
-  system "perl -w \"$mirabelle_home/lib/scripts/report.pl\" \"$log_file\"";
-}
+my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
+  "-e 'use \"$root_file\";' -q $mirabelle_logic" . $quiet;
+
+print "Finished:  $thy_file\n" if ($quiet ne "");
 
 
 # cleanup

--- a/src/HOL/Mirabelle/lib/scripts/report.pl	Fri Sep 04 13:57:56 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-#
-# Author: Sascha Boehme
-#
-# Reports for Mirabelle
-#
-
-my $log_file = $ARGV[0];
-
-open(FILE, "<$log_file") || die "Cannot open file '$log_file'";
-my @lines = <FILE>;
-close(FILE);
-
-my $unhandled = 0;
-
-my $sh_calls = 0;
-my $sh_succeeded = 0;
-my $sh_time = 0;
-
-my $metis_calls = 0;
-my $metis_succeeded = 0;
-my $metis_timeout = 0;
-my $metis_time = 0;
-
-foreach (@lines) {
-  if (m/^unhandled exception/) {
-    $unhandled++;
-  }
-  if (m/^sledgehammer:/) {
-    $sh_calls++;
-  }
-  if (m/^sledgehammer: succeeded \(([0-9]+)\)/) {
-    $sh_succeeded++;
-    $sh_time += $1;
-  }
-  if (m/^metis \(sledgehammer\):/) {
-    $metis_calls++;
-  }
-  if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) {
-    $metis_succeeded++;
-    $metis_time += $1;
-  }
-  if (m/^metis \(sledgehammer\): timeout/) {
-    $metis_timeout++;
-  }
-}
-
-open(FILE, ">>$log_file") || die "Cannot open file '$log_file'";
-
-print FILE "\n\n\n";
-
-if ($unhandled > 0) {
-  print FILE "Number of unhandled exceptions: $unhandled\n\n";
-}
-
-if ($sh_calls > 0) {
-  my $percent = $sh_succeeded / $sh_calls * 100;
-  my $time = $sh_time / 1000;
-  my $avg_time = $time / $sh_succeeded;
-  print FILE "Total number of sledgehammer calls: $sh_calls\n";
-  print FILE "Number of successful sledgehammer calls:  $sh_succeeded\n";
-  printf FILE "Success rate: %.0f%%\n", $percent;
-  printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time;
-  printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time;
-}
-
-if ($metis_calls > 0) {
-  my $percent = $metis_succeeded / $metis_calls * 100;
-  my $time = $metis_time / 1000;
-  my $avg_time = $time / $metis_succeeded;
-  my $metis_exc = $sh_succeeded - $metis_succeeded - $metis_timeout;
-  print FILE "Total number of metis calls: $metis_calls\n";
-  print FILE "Number of successful metis calls: $metis_succeeded\n";
-  print FILE "Number of metis timeouts: $metis_timeout\n";
-  print FILE "Number of metis exceptions: $metis_exc\n";
-  printf FILE "Success rate: %.0f%%\n", $percent;
-  printf FILE "Total time for successful metis calls: %.3f seconds\n", $time;
-  printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time;
-}
-
-close(FILE);