# 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" ^