# HG changeset patch # User blanchet # Date 1379709570 -7200 # Node ID 4d34e267fba9c38474bb97d272b09adcc06f3ecf # Parent cf37f4b84824c284720402994e5255bc4660cce2 use configuration mechanism for low-level tracing diff -r cf37f4b84824 -r 4d34e267fba9 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 20 22:39:30 2013 +0200 @@ -100,8 +100,7 @@ ("isar_minimize", "true"), (* TODO: document *) ("slice", "true"), ("minimize", "smart"), - ("preplay_timeout", "3"), - ("preplay_trace", "false")] (* TODO: document *) + ("preplay_timeout", "3")] val alias_params = [("prover", ("provers", [])), (* undocumented *) @@ -120,8 +119,7 @@ ("dont_slice", "slice"), ("dont_minimize", "minimize"), ("dont_try0_isar", "isar_try0"), - ("dont_minimize_isar", "isar_minimize"), - ("no_preplay_trace", "preplay_trace")] (* TODO: document *) + ("dont_minimize_isar", "isar_minimize")] val params_not_for_minimize = ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", @@ -318,7 +316,6 @@ val preplay_timeout = if mode = Auto_Try then SOME Time.zeroTime else lookup_time "preplay_timeout" - val preplay_trace = lookup_bool "preplay_trace" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, @@ -331,7 +328,7 @@ merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - preplay_trace = preplay_trace, expect = expect} + expect = expect} end fun get_params mode = extract_params mode o default_raw_params diff -r cf37f4b84824 -r 4d34e267fba9 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Sep 20 22:39:30 2013 +0200 @@ -58,9 +58,8 @@ fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, isar_compress, - isar_compress_degree, merge_timeout_slack, - isar_try0, isar_minimize, - preplay_timeout, preplay_trace, ...} : params) + isar_compress_degree, merge_timeout_slack, isar_try0, + isar_minimize, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let val _ = @@ -86,8 +85,7 @@ merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = false, minimize = SOME false, timeout = timeout, - preplay_timeout = preplay_timeout, preplay_trace = preplay_trace, - expect = ""} + preplay_timeout = preplay_timeout, expect = ""} val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} @@ -258,8 +256,8 @@ lam_trans, uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0, - isar_minimize, slice, - minimize, timeout, preplay_timeout, preplay_trace, expect} : params) = + isar_minimize, slice, minimize, timeout, preplay_timeout, expect} : + params) = let fun lookup_override name default_value = case AList.lookup (op =) override_params name of @@ -277,10 +275,9 @@ 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_compress_degree = isar_compress_degree, - merge_timeout_slack = merge_timeout_slack, - isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, - minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, - preplay_trace = preplay_trace, expect = expect} + merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0, + isar_minimize = isar_minimize, slice = slice, minimize = minimize, + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun maybe_minimize ctxt mode do_learn name diff -r cf37f4b84824 -r 4d34e267fba9 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Sep 20 22:39:30 2013 +0200 @@ -17,12 +17,11 @@ PplFail of exn | PplSucc of preplay_time + val trace : bool Config.T val zero_preplay_time : preplay_time val some_preplay_time : preplay_time val add_preplay_time : preplay_time -> preplay_time -> preplay_time val string_of_preplay_time : preplay_time -> string - (*val preplay_raw : bool -> bool -> string -> string -> Proof.context -> - Time.time -> isar_step -> preplay_time*) type preplay_interface = { get_preplay_result : label -> preplay_result, @@ -34,9 +33,8 @@ overall_preplay_stats : isar_proof -> preplay_time * bool } val proof_preplay_interface : - bool -> Proof.context -> string -> string -> bool -> Time.time -> bool + bool -> Proof.context -> string -> string -> bool -> Time.time -> isar_proof -> preplay_interface - end structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY = @@ -45,6 +43,9 @@ open Sledgehammer_Util open Sledgehammer_Proof +val trace = + Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false) + (* The boolean flag encodes whether the time is exact (false) or an lower bound (true): (t, false) = "t ms" @@ -77,7 +78,7 @@ |> nr_of_assms>0 ? cons (Pretty.str "\") |> cons assms |> cons time - val pretty_trace = Pretty.blk(2, Pretty.breaks trace_list) + val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list) in tracing (Pretty.string_of pretty_trace) end (* timing *) @@ -132,8 +133,8 @@ (* main function for preplaying isar_steps; may throw exceptions *) -fun preplay_raw _ _ _ _ _ _ (Let _) = zero_preplay_time - | preplay_raw debug trace type_enc lam_trans ctxt timeout +fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time + | preplay_raw debug type_enc lam_trans ctxt timeout (Prove (_, Fix xs, _, t, subproofs, By (fact_names, proof_method))) = let val (prop, obtain) = @@ -171,12 +172,12 @@ val preplay_time = take_time timeout run_tac () in (* tracing *) - (if trace then preplay_trace ctxt facts prop preplay_time else () ; + (if Config.get ctxt trace then preplay_trace ctxt facts prop preplay_time + else (); preplay_time) end - (*** proof preplay interface ***) type preplay_interface = @@ -216,13 +217,12 @@ The preplay results are caluclated lazyly and cached to avoid repeated calculation. - PRE CONDITION: the proof must be labeled canocially, see + PRECONDITION: the proof must be labeled canocially, see Slegehammer_Proof.relabel_proof_canonically *) - fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay - preplay_timeout preplay_trace proof : preplay_interface = + preplay_timeout proof : preplay_interface = if not do_preplay then (* the dont_preplay option pretends that everything works just fine *) { get_preplay_result = K (PplSucc zero_preplay_time), @@ -238,7 +238,7 @@ val ctxt = enrich_context proof ctxt fun preplay quietly timeout step = - preplay_raw debug preplay_trace type_enc lam_trans ctxt timeout step + preplay_raw debug type_enc lam_trans ctxt timeout step |> PplSucc handle exn => if Exn.is_interrupt exn then diff -r cf37f4b84824 -r 4d34e267fba9 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200 @@ -44,7 +44,6 @@ minimize : bool option, timeout : Time.time option, preplay_timeout : Time.time option, - preplay_trace : bool, expect : string} type relevance_fudge = @@ -359,7 +358,6 @@ minimize : bool option, timeout : Time.time option, preplay_timeout : Time.time option, - preplay_trace : bool, expect : string} type relevance_fudge = @@ -682,8 +680,7 @@ uncurried_aliases, fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0, - isar_minimize, slice, timeout, preplay_timeout, - preplay_trace, ...}) + isar_minimize, slice, timeout, preplay_timeout, ...}) minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let @@ -958,10 +955,10 @@ else () val isar_params = - (debug, verbose, preplay_timeout, preplay_trace, - isar_compress, isar_compress_degree, merge_timeout_slack, - isar_try0, isar_minimize, pool, fact_names, lifted, sym_tab, - atp_proof, goal) + (debug, verbose, preplay_timeout, isar_compress, + isar_compress_degree, merge_timeout_slack, isar_try0, + isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof, + goal) val one_line_params = (preplay, proof_banner mode name, used_facts, choose_minimize_command ctxt params minimize_command name diff -r cf37f4b84824 -r 4d34e267fba9 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200 @@ -12,7 +12,7 @@ type one_line_params = Sledgehammer_Print.one_line_params type isar_params = - bool * bool * Time.time option * bool * real * int * real * bool * bool + bool * bool * Time.time option * real * int * real * bool * bool * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table * string atp_proof * thm @@ -408,14 +408,14 @@ in chain_proof end type isar_params = - bool * bool * Time.time option * bool * real * int * real * bool * bool + bool * bool * Time.time option * real * int * real * bool * bool * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table * string atp_proof * thm fun isar_proof_text ctxt isar_proofs - (debug, verbose, preplay_timeout, preplay_trace, isar_compress, - isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool, - fact_names, lifted, sym_tab, atp_proof, goal) + (debug, verbose, preplay_timeout, isar_compress, isar_compress_degree, + merge_timeout_slack, isar_try0, isar_minimize, pool, fact_names, lifted, + sym_tab, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt @@ -580,13 +580,13 @@ chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof - val (preplay_interface as { overall_preplay_stats, ... }, isar_proof) = + val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) = refute_graph |> redirect_graph axioms tainted bot |> isar_proof_of_direct_proof |> relabel_proof_canonically |> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay - preplay_timeout preplay_trace) + preplay_timeout) val ((preplay_time, preplay_fail), isar_proof) = isar_proof |> compress_proof