# HG changeset patch # User blanchet # Date 1447680430 -3600 # Node ID 95a57e288fd4b6d2315385ee463b4e494ebc5194 # Parent e6784939d6455712a74b282eca596d2c67c6ec60 more tracing in MaSh diff -r e6784939d645 -r 95a57e288fd4 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Nov 16 13:08:52 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Nov 16 14:27:10 2015 +0100 @@ -1491,10 +1491,13 @@ fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover = let + val _ = trace_msg ctxt (fn () => "Extracting clasimpset...") val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val ctxt = ctxt |> Config.put instantiate_inducts false + val _ = trace_msg ctxt (fn () => "Extracting facts...") val facts = nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True} + |> tap (fn _ => trace_msg ctxt (fn () => "Sorting facts...")) |> sort (crude_thm_ord ctxt o apply2 snd o swap) val num_facts = length facts val prover = hd provers @@ -1502,6 +1505,7 @@ fun learn auto_level run_prover = mash_learn_facts ctxt params prover auto_level run_prover one_year facts |> writeln + val _ = trace_msg ctxt (fn () => "MaShing...") in if run_prover then (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^