# HG changeset patch # User blanchet # Date 1307515663 -7200 # Node ID a4aeb26a63624720b5bff50c9bcab5673c125759 # Parent 7b875e14b90d4ed7992e5df79a38869b850d9717 make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization diff -r 7b875e14b90d -r a4aeb26a6362 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jun 08 08:47:43 2011 +0200 @@ -400,9 +400,9 @@ fun failed failure = ({outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE, preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis), - message = K ""}, ~1) - val ({outcome, used_facts, run_time_in_msecs, preplay, message} - : Sledgehammer_Provers.prover_result, + message = K "", message_tail = ""}, ~1) + val ({outcome, used_facts, run_time_in_msecs, preplay, message, + message_tail} : Sledgehammer_Provers.prover_result, time_isa) = time_limit (Mirabelle.cpu_time (fn () => let val _ = if is_appropriate_prop concl_t then () @@ -421,7 +421,7 @@ handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time_in_msecs |> the_default ~1 - val msg = message (preplay ()) + val msg = message (preplay ()) ^ message_tail in case outcome of NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) @@ -515,8 +515,9 @@ Sledgehammer_Minimize.minimize_facts prover_name params true 1 (Sledgehammer_Util.subgoal_count st) val _ = log separator - val (used_facts, (preplay, message)) = minimize st (these (!named_thms)) - val msg = message (preplay ()) + val (used_facts, (preplay, message, message_tail)) = + minimize st (these (!named_thms)) + val msg = message (preplay ()) ^ message_tail in case used_facts of SOME named_thms' => diff -r 7b875e14b90d -r a4aeb26a6362 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200 @@ -16,7 +16,7 @@ string -> params -> bool -> int -> int -> Proof.state -> ((string * locality) * thm list) list -> ((string * locality) * thm list) list option - * ((unit -> play) * (play -> string)) + * ((unit -> play) * (play -> string) * string) val run_minimize : params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit end; @@ -167,7 +167,7 @@ Int.min (msecs, Time.toMilliseconds time + slack_msecs) |> Time.fromMilliseconds val facts = filter_used_facts used_facts facts - val (min_thms, {preplay, message, ...}) = + val (min_thms, {preplay, message, message_tail, ...}) = if length facts >= Config.get ctxt binary_min_facts then binary_minimize (do_test new_timeout) facts else @@ -178,17 +178,18 @@ (case length (filter (curry (op =) Chained o snd o fst) min_thms) of 0 => "" | n => " (including " ^ string_of_int n ^ " chained)") ^ ".") - in (SOME min_thms, (preplay, message)) end + in (SOME min_thms, (preplay, message, message_tail)) end | {outcome = SOME TimedOut, preplay, ...} => (NONE, (preplay, fn _ => "Timeout: You can increase the time limit using the \ \\"timeout\" option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ "\").")) + string_of_int (10 + msecs div 1000) ^ "\").", + "")) | {preplay, message, ...} => - (NONE, (preplay, prefix "Prover error: " o message))) + (NONE, (preplay, prefix "Prover error: " o message, ""))) handle ERROR msg => - (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg)) + (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, "")) end fun run_minimize (params as {provers, ...}) i refs state = @@ -207,8 +208,9 @@ | prover :: _ => (kill_provers (); minimize_facts prover params false i n state facts - |> (fn (_, (preplay, message)) => - Output.urgent_message (message (preplay ())))) + |> (fn (_, (preplay, message, message_tail)) => + message (preplay ()) ^ message_tail + |> Output.urgent_message)) end end; diff -r 7b875e14b90d -r a4aeb26a6362 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 08 08:47:43 2011 +0200 @@ -57,7 +57,8 @@ used_facts: (string * locality) list, run_time_in_msecs: int option, preplay: unit -> play, - message: play -> string} + message: play -> string, + message_tail: string} type prover = params -> (string -> minimize_command) -> prover_problem -> prover_result @@ -324,7 +325,8 @@ used_facts: (string * locality) list, run_time_in_msecs: int option, preplay: unit -> play, - message: play -> string} + message: play -> string, + message_tail: string} type prover = params -> (string -> minimize_command) -> prover_problem -> prover_result @@ -774,7 +776,7 @@ extract_important_message output else "" - val (used_facts, preplay, message) = + val (used_facts, preplay, message, message_tail) = case outcome of NONE => let @@ -803,25 +805,23 @@ (preplay, proof_banner mode name, used_facts, choose_minimize_command minimize_command name preplay, subgoal, subgoal_count) - in - proof_text ctxt isar_proof isar_params one_line_params ^ - (if verbose then - "\nATP real CPU time: " ^ - string_from_time (Time.fromMilliseconds (the msecs)) ^ "." - else - "") ^ - (if important_message <> "" then - "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ - important_message - else - "") - end) + in proof_text ctxt isar_proof isar_params one_line_params end, + (if verbose then + "\nATP real CPU time: " ^ + string_from_time (Time.fromMilliseconds (the msecs)) ^ "." + else + "") ^ + (if important_message <> "" then + "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ + important_message + else + "")) end | SOME failure => - ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure) + ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "") in {outcome = outcome, used_facts = used_facts, run_time_in_msecs = msecs, - preplay = preplay, message = message} + preplay = preplay, message = message, message_tail = message_tail} end (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until @@ -974,7 +974,7 @@ smt_filter_loop ctxt name params state subgoal smt_filter facts val (used_facts, used_ths) = used_facts |> ListPair.unzip val outcome = outcome |> Option.map failure_from_smt_failure - val (preplay, message) = + val (preplay, message, message_tail) = case outcome of NONE => (fn () => @@ -994,21 +994,19 @@ (preplay, proof_banner mode name, used_facts, choose_minimize_command minimize_command name preplay, subgoal, subgoal_count) - in - one_line_proof_text one_line_params ^ - (if verbose then - "\nSMT solver real CPU time: " ^ - string_from_time (Time.fromMilliseconds - (the run_time_in_msecs)) ^ "." - else - "") - end) + in one_line_proof_text one_line_params end, + if verbose then + "\nSMT solver real CPU time: " ^ + string_from_time (Time.fromMilliseconds + (the run_time_in_msecs)) ^ "." + else + "") | SOME failure => - (K (Failed_to_Play Metis), fn _ => string_for_failure failure) + (K (Failed_to_Play Metis), fn _ => string_for_failure failure, "") in {outcome = outcome, used_facts = used_facts, run_time_in_msecs = run_time_in_msecs, preplay = preplay, - message = message} + message = message, message_tail = message_tail} end fun run_metis mode name ({debug, timeout, ...} : params) minimize_command @@ -1032,13 +1030,15 @@ val one_line_params = (play, proof_banner mode name, used_facts, minimize_command name, subgoal, subgoal_count) - in one_line_proof_text one_line_params end} + in one_line_proof_text one_line_params end, + message_tail = ""} | play => let val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut in {outcome = SOME failure, used_facts = [], run_time_in_msecs = NONE, - preplay = K play, message = fn _ => string_for_failure failure} + preplay = K play, message = fn _ => string_for_failure failure, + message_tail = ""} end end diff -r 7b875e14b90d -r a4aeb26a6362 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jun 08 08:47:43 2011 +0200 @@ -76,7 +76,7 @@ fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...}) ({state, subgoal, subgoal_count, facts, ...} : prover_problem) (result as {outcome, used_facts, run_time_in_msecs, preplay, - message} : prover_result) = + message, message_tail} : prover_result) = if is_some outcome then result else @@ -112,7 +112,7 @@ end else ((false, name), preplay) - val (used_facts, (preplay, message)) = + val (used_facts, (preplay, message, _)) = if minimize then minimize_facts minimize_name params (not verbose) subgoal subgoal_count state @@ -120,7 +120,7 @@ (map (apsnd single o untranslated_fact) facts)) |>> Option.map (map fst) else - (SOME used_facts, (preplay, message)) + (SOME used_facts, (preplay, message, "")) in case used_facts of SOME used_facts => @@ -137,7 +137,7 @@ (); {outcome = NONE, used_facts = used_facts, run_time_in_msecs = run_time_in_msecs, preplay = preplay, - message = message}) + message = message, message_tail = message_tail}) | NONE => result end @@ -167,10 +167,10 @@ fun really_go () = problem |> get_minimizing_prover ctxt mode name params minimize_command - |> (fn {outcome, preplay, message, ...} => + |> (fn {outcome, preplay, message, message_tail, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN - else someN, message o preplay)) + else someN, fn () => message (preplay ()) ^ message_tail)) fun go () = let val (outcome_code, message) =