# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID fada390d49ddb880543a5ce2f5a51936fc17798f
# Parent  094ba0948403742258f6e5b785d2fc32796d3ee3
tweaked Auto Sledgehammer's behavior and output

diff -r 094ba0948403 -r fada390d49dd src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -252,9 +252,12 @@
 
     val message = message ()
     val () =
-      (case outcome of
-        SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
-      | _ => ())
+      if mode = Auto_Try then
+        ()
+      else
+        (case outcome of
+          SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
+        | _ => ())
   in
     (outcome, message)
   end
@@ -452,7 +455,7 @@
         |> `(fn (outcome, _) =>
           (case outcome of
             SH_Some _ => (print "QED"; true)
-          | _ => (print "Sorry"; false)))
+          | _ => (print "No proof found"; false)))
       end)
 
 end;
diff -r 094ba0948403 -r fada390d49dd src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -170,7 +170,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value ctxt =
-  filter (is_prover_installed ctxt) (atps @ smts ctxt) \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
+  filter (is_prover_installed ctxt) (smts ctxt @ atps) \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
   |> implode_param
 
 fun set_default_raw_param param thy =
@@ -261,7 +261,7 @@
     val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
     val smt_proofs = lookup_bool "smt_proofs"
-    val minimize = lookup_bool "minimize"
+    val minimize = mode <> Auto_Try andalso lookup_bool "minimize"
     val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices")
     val timeout = lookup_time "timeout"
     val preplay_timeout = lookup_time "preplay_timeout"
diff -r 094ba0948403 -r fada390d49dd src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -183,8 +183,7 @@
 
 fun try_command_line banner play command =
   let val s = string_of_play_outcome play in
-    banner ^ Active.sendback_markup_command command ^
-    (s |> s <> "" ? enclose " (" ")")
+    banner ^ Active.sendback_markup_command command ^ (s |> s <> "" ? enclose " (" ")")
   end
 
 fun one_line_proof_text _ num_chained
diff -r 094ba0948403 -r fada390d49dd src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -194,7 +194,7 @@
   (case mode of
     Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: "
   | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: "
-  | _ => "")
+  | _ => "Try this: ")
 
 fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans =
   let
diff -r 094ba0948403 -r fada390d49dd src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -38,7 +38,7 @@
 val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true)
 val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true)
 
-val smts = SMT_Config.all_solvers_of
+val smts = sort_strings o SMT_Config.all_solvers_of
 
 val is_smt_prover = member (op =) o smts
 val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of