clarify Sledgehammer instantiations without preplay (dont_preplay option and tactic provers)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon May 12 13:02:52 2025 +0200
@@ -145,17 +145,15 @@
      end)
   |> sort (play_outcome_ord o apply2 (fn (_, (play_outcome, _)) => play_outcome))
 
-fun select_one_line_proof used_facts preferred_meth preplay_results =
+fun select_one_line_proof preferred_meth preplay_results =
   (case preplay_results of
     (* Select best method if preplay succeeded *)
     (best_meth, (best_outcome as Played _, best_used_facts)) :: _ =>
-    (best_used_facts, (best_meth, best_outcome))
+    SOME (best_used_facts, (best_meth, best_outcome))
     (* Otherwise select preferred method *)
   | _ =>
-    (used_facts, (preferred_meth,
-       (case AList.lookup (op =) preplay_results preferred_meth of
-         SOME (outcome, _) => outcome
-       | NONE => Play_Timed_Out Time.zeroTime))))
+    AList.lookup (op =) preplay_results preferred_meth
+    |> Option.map (fn (outcome, used_facts) => (used_facts, (preferred_meth, outcome))))
 
 fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
     (problem as {state, subgoal, factss, ...} : prover_problem)
@@ -225,55 +223,59 @@
 fun preplay_prover_result ({verbose, instantiate, minimize, preplay_timeout, ...} : params)
     state goal subgoal
     (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
-  let
-    val used_facts0 = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts
-    val pretty_used_facts0 = map (apfst Pretty.str) used_facts0
-    val (output, pretty_used_facts, preplay_results) =
-      if outcome = SOME ATP_Proof.TimedOut then
-        (SH_TimeOut, pretty_used_facts0, [])
-      else if outcome = SOME ATP_Proof.OutOfResources then
-        (SH_ResourcesOut, pretty_used_facts0, [])
-      else if is_some outcome then
-        (SH_None, pretty_used_facts0, [])
-      else
-        let
-          val preplay = `(fn pretty_used_facts =>
-            play_one_line_proofs minimize preplay_timeout pretty_used_facts
-              state goal subgoal (snd preferred_methss))
-          fun preplay_succeeded ((_, (Played _, _)) :: _, _) _ = true
-            | preplay_succeeded _ [] = true
-            | preplay_succeeded _ _ = false
-          val instantiate_timeout = Time.scale 5.0 preplay_timeout
-          val instantiate = if null used_facts0 then SOME false else instantiate
-          val (preplay_results, pretty_used_facts) =
-            (case instantiate of
-              SOME false => preplay pretty_used_facts0
-            | SOME true =>
-              (* Always try to infer variable instantiations *)
+  if outcome = SOME ATP_Proof.TimedOut then
+    (SH_TimeOut, fn () => message NONE)
+  else if outcome = SOME ATP_Proof.OutOfResources then
+    (SH_ResourcesOut, fn () => message NONE)
+  else if is_some outcome then
+    (SH_None, fn () => message NONE)
+  else
+    let
+      val used_facts0 = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts
+      val pretty_used_facts0 = map (apfst Pretty.str) used_facts0
+      fun preplay methss pretty_used_facts =
+        play_one_line_proofs minimize preplay_timeout pretty_used_facts state goal subgoal methss
+      fun preplay_succeeded ((_, (Played _, _)) :: _) = true
+        | preplay_succeeded _ = false
+      val instantiate_timeout =
+        if preplay_timeout = Time.zeroTime then
+          Time.fromSeconds 5
+        else
+          Time.scale 5.0 preplay_timeout
+      val instantiate = if null used_facts0 then SOME false else instantiate
+      val preplay_results =
+        (case instantiate of
+          SOME false => preplay (snd preferred_methss) pretty_used_facts0
+        | SOME true =>
+          (* Always try to infer variable instantiations *)
+          (case instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0 of
+            NONE => preplay (snd preferred_methss) pretty_used_facts0
+          | SOME pretty_used_facts =>
+            if preplay_timeout = Time.zeroTime then
+              [(fst preferred_methss, (Play_Timed_Out Time.zeroTime, pretty_used_facts))]
+            else if null (snd preferred_methss) then
+              preplay [[fst preferred_methss]] pretty_used_facts
+            else
+              preplay (snd preferred_methss) pretty_used_facts)
+        | NONE =>
+          let
+            val preplay_results0 = preplay (snd preferred_methss) pretty_used_facts0
+            val preplay_disabled =
+              preplay_timeout = Time.zeroTime orelse null (snd preferred_methss)
+          in
+            if preplay_succeeded preplay_results0 orelse preplay_disabled then
+              preplay_results0
+            else
+              (* Preplay failed, now try to infer variable instantiations *)
               instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0
-              |> the_default pretty_used_facts0
-              |> preplay
-            | NONE =>
-              let
-                val preplay_results0 = preplay pretty_used_facts0
-              in
-                if preplay_succeeded preplay_results0 (snd preferred_methss) then
-                  preplay_results0
-                else
-                  (* Preplay failed, now try to infer variable instantiations *)
-                  instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0
-                  |> Option.map preplay
-                  |> the_default preplay_results0
-              end)
-        in
-          (SH_Some (result, preplay_results), pretty_used_facts, preplay_results)
-        end
-    fun chosen_preplay_outcome () =
-      select_one_line_proof pretty_used_facts (fst preferred_methss) preplay_results
-    fun output_message () = message chosen_preplay_outcome
-  in
-    (output, output_message)
-  end
+              |> Option.map (preplay (snd preferred_methss))
+              |> the_default preplay_results0
+          end)
+      fun output_message () =
+        message (select_one_line_proof (fst preferred_methss) preplay_results)
+    in
+      (SH_Some (result, preplay_results), output_message)
+    end
 
 fun analyze_prover_result_for_inconsistency (result as {outcome, used_facts, ...} : prover_result) =
   if outcome = SOME ATP_Proof.TimedOut then

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon May 12 13:02:52 2025 +0200
@@ -220,7 +220,6 @@
   | apply_on_subgoal 1 _ = "apply "
   | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
-(* FIXME *)
 fun proof_method_command meth i n extras =
   let
     val (indirect_facts, direct_facts) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon May 12 13:02:52 2025 +0200
@@ -82,7 +82,7 @@
      used_from : fact list,
      preferred_methss : proof_method * proof_method list list,
      run_time : Time.time,
-     message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
+     message : ((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string}
 
   type prover = params -> prover_problem -> prover_slice -> prover_result
 
@@ -210,7 +210,7 @@
    used_from : fact list,
    preferred_methss : proof_method * proof_method list list,
    run_time : Time.time,
-   message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
+   message : ((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string}
 
 type prover = params -> prover_problem -> prover_slice -> prover_result
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon May 12 13:02:52 2025 +0200
@@ -334,7 +334,7 @@
                bunches_of_metis_methods ctxt needs_full_types needs_lam_defs)
         in
           (NONE, used_facts, preferred_methss,
-           fn preplay =>
+           fn preplay_outcome =>
               let
                 val _ = if verbose then writeln "Generating proof text..." else ()
 
@@ -361,7 +361,11 @@
                      try0, minimize, full_atp_proof, goal)
                   end
 
-                val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
+                val preplay_result = preplay_outcome
+                  |> the_default
+                    (map (apfst Pretty.str) used_facts,
+                     (preferred, Play_Timed_Out Time.zeroTime))
+                val one_line_params = (preplay_result, proof_banner mode name, subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
                 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon May 12 13:02:52 2025 +0200
@@ -25,7 +25,7 @@
   val minimize_facts : (thm list -> unit) -> string -> params -> prover_slice -> bool -> int ->
     int -> Proof.state -> thm -> ((string * stature) * thm list) list -> prover_result ->
     ((string * stature) * thm list) list option
-    * ((unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string)
+    * (((Pretty.T * stature) list * (proof_method * play_outcome)) option -> string)
   val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
 end;
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon May 12 13:02:52 2025 +0200
@@ -153,7 +153,7 @@
               bunches_of_metis_methods ctxt false true
         in
           ((preferred, methss),
-           fn preplay =>
+           fn preplay_outcome =>
              let
                val _ = if verbose then writeln "Generating proof text..." else ()
 
@@ -161,7 +161,11 @@
                  (verbose, (NONE, NONE, []), preplay_timeout, compress, try0, minimize,
                   atp_proof (), goal)
 
-               val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
+                val preplay_result = preplay_outcome
+                  |> the_default
+                    (map (apfst Pretty.str) used_facts,
+                     (preferred, Play_Timed_Out Time.zeroTime))
+               val one_line_params = (preplay_result, proof_banner mode name, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Sun May 11 12:05:10 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Mon May 12 13:02:52 2025 +0200
@@ -98,9 +98,17 @@
         NONE => (found_something name; map fst facts)
       | SOME _ => [])
 
-    val message = fn _ =>
+    val message = fn preplay_outcome =>
       (case outcome of
-        NONE => try_command_line (proof_banner mode name) (Played run_time) command
+        NONE =>
+        let
+          val banner = proof_banner mode name
+        in
+          (case preplay_outcome of
+            NONE => try_command_line banner (Played run_time) command
+          | SOME preplay_result =>
+              one_line_proof_text (preplay_result, banner, subgoal, subgoal_count))
+        end
       | SOME failure => string_of_atp_failure failure)
   in
     {outcome = outcome, used_facts = used_facts, used_from = facts,