# HG changeset patch
# User desharna
# Date 1642847611 -3600
# Node ID ef18787842b315ce4379b63fc33e35cbc0ce8e15
# Parent  d9a5824f68c8edd75c60e1946b6fb73c3a99cc46
added spying of fact filtering timing

diff -r d9a5824f68c8 -r ef18787842b3 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Jan 22 08:46:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Jan 22 11:33:31 2022 +0100
@@ -310,14 +310,17 @@
         val inst_inducts = induction_rules = SOME Instantiate
         val {facts = chained_thms, goal, ...} = Proof.goal state
         val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
-        val all_facts =
-          nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts concl_t
         val _ =
           (case find_first (not o is_prover_supported ctxt) provers of
             SOME name => error ("No such prover: " ^ name)
           | NONE => ())
         val _ = print "Sledgehammering..."
         val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
+        val ({elapsed, ...}, all_facts) = Timing.timing
+          (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t
+        val _ = spying spy (fn () => (state, i, "All",
+          "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^
+          string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
 
         val spying_str_of_factss =
           commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
@@ -334,9 +337,8 @@
               (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t)
               all_facts
             val () = spying spy (fn () => (state, i, "All",
-              "Filtering " ^ string_of_int (length all_facts) ^ " facts in " ^
-              string_of_int (Time.toMilliseconds elapsed) ^ " ms (MaSh algorithm: " ^
-              str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
+              "Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^
+              " ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
             val () = if verbose then print (string_of_factss factss) else ()
             val () = spying spy (fn () =>
               (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))
diff -r d9a5824f68c8 -r ef18787842b3 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 22 08:46:37 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 22 11:33:31 2022 +0100
@@ -531,8 +531,7 @@
     ||> op @ |> op @
   end
 
-fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts
-    concl_t =
+fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t =
   if only andalso null add then
     []
   else