--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Sep 04 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sat Sep 05 17:35:05 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 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Sat Sep 05 17:35:05 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 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Sat Sep 05 17:35:05 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 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Sat Sep 05 17:35:05 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 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Sep 05 17:35:05 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), atp_time, _, _, _), sh_time) =
+ TimeLimit.timeLimit timeout (Mirabelle.cpu_time atp) (Proof.get_goal st)
+ in
+ if success then (message, SOME (atp_time, sh_time, thm_names))
+ else (message, NONE)
+ end
+ handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, 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
+ in
+ (case result of
+ SOME (atp_time, sh_time, names) =>
+ let
+ val _ = change_data id inc_sh_success
+ val _ = change_data id (inc_sh_time (atp_time + sh_time))
+ val _ = change thm_names (K (SOME names))
+ in
+ log (sh_tag id ^ "succeeded (" ^ string_of_int atp_time ^ "+" ^
+ string_of_int sh_time ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
+ end
+ | NONE => log (sh_tag id ^ "failed: " ^ msg))
+ 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/doc/options.txt Fri Sep 04 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt Sat Sep 05 17:35:05 2009 +0200
@@ -2,6 +2,5 @@
* prover=NAME: name of the external prover to call
* keep=PATH: path where to keep temporary files created by sledgehammer
- * metis=X: apply metis with the theorems found by sledgehammer (X may be any
- non-empty string)
- * full_types=X: turn on full-typed encoding (X may be any non-empty string)
+ * metis: apply metis with the theorems found by sledgehammer
+ * full_types: turn on full-typed encoding
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Fri Sep 04 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Sat Sep 05 17:35:05 2009 +0200
@@ -26,14 +26,18 @@
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."
echo
echo " ACTIONS is a colon-separated list of actions, where each action is"
- echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
+ echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:"
print_action_names
echo
+ echo " A list of available OPTIONs can be found here:"
+ echo " $MIRABELLE_HOME/doc/options.txt"
+ echo
echo " FILES is a list of theory files, where each file is either NAME.thy"
echo " or NAME.thy[START:END] and START and END are numbers indicating the"
echo " range the given actions are to be applied."
@@ -46,7 +50,7 @@
# options
-while getopts "L:T:O:t:?" OPT
+while getopts "L:T:O:t:q?" OPT
do
case "$OPT" in
L)
@@ -61,15 +65,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 +92,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 15:19:51 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Sat Sep 05 17:35:05 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]+)\]$/) {
@@ -82,6 +82,10 @@
print SETUP_FILE "$sep(\"$1\", \"$2\")";
$sep = ", ";
}
+ elsif (m/\s*(.*)\s*/) {
+ print SETUP_FILE "$sep(\"$1\", \"\")";
+ $sep = ", ";
+ }
}
print SETUP_FILE "] *}\n";
}
@@ -122,15 +126,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 15:19:51 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);