src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

 val atp_important_message_keep_quotient = 25
 
 fun run_atp mode name
     ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
      max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
-     slice, minimize, timeout, preplay_timeout, ...} : params)
+     slice, minimize, timeout, preplay_timeout, spy, ...} : params)
     ({comment, state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 

                 " with " ^ string_of_int num_facts ^ " fact" ^
                 plural_s num_facts ^ " for " ^ string_of_time slice_timeout ^ "..."
                 |> writeln
               else
                 ()
-            val value as (atp_problem, _, _, _) =
+            val ({elapsed, ...}, value as (atp_problem, _, _, _)) = Timing.timing (fn () =>
               if cache_key = SOME key then
                 cache_value
               else
                 let
                   val sound = is_type_enc_sound type_enc

                   |> take num_facts
                   |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
                   |> map (apsnd Thm.prop_of)
                   |> generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
                     lam_trans uncurried_aliases readable_names true hyp_ts concl_t
-                end
+                end) ()
+
+            val () = spying spy (fn () =>
+              (state, subgoal, name, "Slice #" ^ string_of_int (slice + 1) ^
+               " generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms"))
 
             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem
 
             val ord = effective_term_order ctxt name

                  |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name)
                    atp_problem
                  handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
               handle Timeout.TIMEOUT _ => (("", slice_timeout), ([], SOME TimedOut))
                 | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg)))
+
+            val () = spying spy (fn () =>
+              (state, subgoal, name, "Slice #" ^ string_of_int (slice + 1) ^
+               " running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms"))
 
             val outcome =
               (case outcome of
                 NONE =>
                 (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of