# HG changeset patch # User blanchet # Date 1379940823 -7200 # Node ID ac1ec50653164b62073edf1ab67ed0793e819d1a # Parent 784223a8576ecaf1cf4282a1df0ce9362da9ffb4 added "spy" option to Sledgehammer diff -r 784223a8576e -r ac1ec5065316 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Mon Sep 23 13:34:15 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Mon Sep 23 14:53:43 2013 +0200 @@ -56,7 +56,11 @@ structure ATP_Util : ATP_UTIL = struct -val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now +fun timestamp_format time = + Date.fmt "%Y-%m-%d %H:%M:%S." (Date.fromTimeLocal time) ^ + (StringCvt.padLeft #"0" 3 (string_of_int (Time.toMilliseconds time - 1000 * Time.toSeconds time))) + +val timestamp = timestamp_format o Time.now (* This hash function is recommended in "Compilers: Principles, Techniques, and Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they diff -r 784223a8576e -r ac1ec5065316 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 23 13:34:15 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Sep 23 14:53:43 2013 +0200 @@ -81,6 +81,7 @@ [("debug", "false"), ("verbose", "false"), ("overlord", "false"), + ("spy", "false"), ("blocking", "false"), ("type_enc", "smart"), ("strict", "false"), @@ -108,6 +109,7 @@ [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), + ("dont_spy", "spy"), ("non_blocking", "blocking"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), @@ -184,7 +186,10 @@ structure Data = Theory_Data ( type T = raw_param list - val empty = default_default_params |> map (apsnd single) + val empty = + default_default_params + |> getenv "SLEDGEHAMMER_SPY" = "yes" ? AList.update (op =) ("spy", "true") + |> map (apsnd single) val extend = I fun merge data : T = AList.merge (op =) (K true) data ) @@ -278,6 +283,7 @@ val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" + val spy = lookup_bool "spy" val blocking = Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking" @@ -311,15 +317,13 @@ else lookup_time "preplay_timeout" val expect = lookup_string "expect" in - {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, - provers = provers, type_enc = type_enc, strict = strict, - lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, - learn = learn, fact_filter = fact_filter, max_facts = max_facts, - fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, + {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, + provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, + uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, + max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = expect} + isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, minimize = minimize, + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params diff -r 784223a8576e -r ac1ec5065316 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Sep 23 13:34:15 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Sep 23 14:53:43 2013 +0200 @@ -55,7 +55,7 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) -fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, +fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, isar_compress, isar_try0, preplay_timeout, ...} : params) @@ -73,18 +73,16 @@ val {goal, ...} = Proof.goal state val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = - {debug = debug, verbose = verbose, overlord = overlord, blocking = true, - provers = provers, type_enc = type_enc, strict = strict, - lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, - learn = false, fact_filter = NONE, max_facts = SOME (length facts), - fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, - max_new_mono_instances = max_new_mono_instances, - isar_proofs = isar_proofs, isar_compress = isar_compress, - isar_try0 = isar_try0, slice = false, minimize = SOME false, - timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} + {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true, + provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, + uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, + max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), + max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, + isar_proofs = isar_proofs, isar_compress = isar_compress, isar_try0 = isar_try0, + slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout, + expect = ""} val problem = - {state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)]} + {state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} val result as {outcome, used_facts, run_time, ...} = prover params (K (K (K ""))) problem in @@ -248,7 +246,7 @@ end fun adjust_reconstructor_params override_params - ({debug, verbose, overlord, blocking, provers, type_enc, strict, + ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans, uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, isar_compress, isar_try0, slice, minimize, timeout, preplay_timeout, @@ -263,15 +261,13 @@ val type_enc = lookup_override "type_enc" type_enc val lam_trans = lookup_override "lam_trans" lam_trans in - {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, - provers = provers, type_enc = type_enc, strict = strict, - lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, - learn = learn, fact_filter = fact_filter, max_facts = max_facts, - fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, + {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, + provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, + uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, + max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, - isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - expect = expect} + isar_compress = isar_compress, isar_try0 = isar_try0, slice = slice, minimize = minimize, + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun maybe_minimize ctxt mode do_learn name diff -r 784223a8576e -r ac1ec5065316 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 23 13:34:15 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Sep 23 14:53:43 2013 +0200 @@ -22,6 +22,7 @@ {debug : bool, verbose : bool, overlord : bool, + spy : bool, blocking : bool, provers : string list, type_enc : string option, @@ -333,6 +334,7 @@ {debug : bool, verbose : bool, overlord : bool, + spy : bool, blocking : bool, provers : string list, type_enc : string option, diff -r 784223a8576e -r ac1ec5065316 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 23 13:34:15 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Sep 23 14:53:43 2013 +0200 @@ -30,6 +30,7 @@ open ATP_Util open ATP_Problem_Generate +open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact @@ -64,29 +65,31 @@ (if blocking then "." else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))) -fun launch_prover (params as {debug, verbose, blocking, max_facts, slice, +fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, slice, timeout, expect, ...}) mode output_result minimize_command only learn {state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state + val hard_timeout = time_mult 3.0 (timeout |> the_default one_day) + val _ = spying spy (fn () => (name, "launched")); val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) - val max_facts = - max_facts |> the_default (default_max_facts_of_prover ctxt slice name) + val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt slice name) val num_facts = length facts |> not only ? Integer.min max_facts - fun desc () = - prover_description ctxt params name num_facts subgoal subgoal_count goal + + fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal + val problem = {state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, - factss = - factss + factss = factss |> map (apsnd ((not (is_ho_atp ctxt name) ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) #> take num_facts))} + fun print_used_facts used_facts used_from = tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) @@ -96,6 +99,15 @@ |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ " proof (of " ^ string_of_int (length facts) ^ "): ") "." |> Output.urgent_message + + fun spying_str_of_res {outcome = NONE, used_facts, ...} = + let val num_used_facts = length used_facts in + "success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ + plural_s num_used_facts + end + | spying_str_of_res {outcome = SOME failure, ...} = + "failure: " ^ string_of_atp_failure failure + fun really_go () = problem |> get_minimizing_prover ctxt mode learn name params minimize_command @@ -103,10 +115,13 @@ ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) + |> spy + ? tap (fn res => spying spy (fn () => (name, spying_str_of_res res))) |> (fn {outcome, preplay, message, message_tail, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN else someN, fn () => message (Lazy.force preplay) ^ message_tail)) + fun go () = let val (outcome_code, message) = @@ -182,8 +197,7 @@ |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts) |> space_implode "\n\n" -fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts, - slice, ...}) +fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, slice, ...}) mode output_result i (fact_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." @@ -211,9 +225,14 @@ SOME name => error ("No such prover: " ^ name ^ ".") | NONE => () val _ = print "Sledgehammering..." + val _ = spying spy (fn () => ("***", "run")) val (smts, (ueq_atps, full_atps)) = provers |> List.partition (is_smt_prover ctxt) ||> List.partition (is_unit_equational_atp ctxt) + + val spying_str_of_factss = + commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) + fun get_factss label is_appropriate_prop provers = let val max_max_facts = @@ -223,6 +242,8 @@ 0 |> fold (Integer.max o default_max_facts_of_prover ctxt slice) provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) + val _ = spying spy (fn () => + (label ^ "s", "filtering " ^ string_of_int (length all_facts) ^ " facts")); in all_facts |> (case is_appropriate_prop of @@ -237,7 +258,10 @@ |> print else ()) + |> spy ? tap (fn factss => + spying spy (fn () => (label ^ "s", "selected facts: " ^ spying_str_of_factss factss))) end + fun launch_provers state label is_appropriate_prop provers = let val factss = get_factss label is_appropriate_prop provers @@ -260,6 +284,7 @@ |> (if blocking then Par_List.map else map) (launch problem #> fst) |> max_outcome_code |> rpair state end + fun launch_atps label is_appropriate_prop atps accum = if null atps then accum @@ -274,15 +299,19 @@ accum) else launch_provers state label is_appropriate_prop atps + fun launch_smts accum = if null smts then accum else launch_provers state "SMT solver" NONE smts + val launch_full_atps = launch_atps "ATP" NONE full_atps - val launch_ueq_atps = - launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps + + val launch_ueq_atps = launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps + fun launch_atps_and_smt_solvers () = [launch_full_atps, launch_smts, launch_ueq_atps] |> Par_List.map (fn f => ignore (f (unknownN, state))) handle ERROR msg => (print ("Error: " ^ msg); error msg) + fun maybe f (accum as (outcome_code, _)) = accum |> (mode = Normal orelse outcome_code <> someN) ? f in diff -r 784223a8576e -r ac1ec5065316 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 23 13:34:15 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Sep 23 14:53:43 2013 +0200 @@ -17,6 +17,7 @@ val time_mult : real -> Time.time -> Time.time val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val spying : bool -> (unit -> string * string) -> unit val subgoal_count : Proof.state -> int val reserved_isar_keyword_table : unit -> unit Symtab.table val thms_in_proof : @@ -87,6 +88,15 @@ SOME (seconds (the secs)) end +val spying_version = "a" + +fun spying false _ = () + | spying true f = + let val (tool, message) = f () in + File.append (Path.explode "$ISABELLE_HOME_USER/spy_sledgehammer") + (spying_version ^ " " ^ timestamp () ^ ": " ^ tool ^ ": " ^ message ^ "\n") + end + val subgoal_count = Try.subgoal_count fun reserved_isar_keyword_table () =