merged
authordesharna
Sun, 19 Dec 2021 11:15:21 +0100
changeset 74955 6f5eafd952c9
parent 74954 74c53a9027e2 (diff)
parent 74947 7ada0c20379b (current diff)
child 74956 a7183a0a33e1
merged
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Mirabelle.thy	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Mirabelle.thy	Sun Dec 19 11:15:21 2021 +0100
@@ -13,7 +13,7 @@
 
 ML \<open>
 signature MIRABELLE_ACTION = sig
-  val make_action : Mirabelle.action_context -> Mirabelle.action
+  val make_action : Mirabelle.action_context -> string * Mirabelle.action
 end
 \<close>
 
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -429,8 +429,7 @@
   Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
 val add_schematic_consts_of =
   Term.fold_aterms (fn Const (x as (s, _)) =>
-                       not (member (op =) atp_widely_irrelevant_consts s)
-                       ? add_schematic_const x
+                       not (is_widely_irrelevant_const s) ? add_schematic_const x
                       | _ => I)
 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
 
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -14,7 +14,7 @@
   type command =
     {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}
   type action = {run_action: command -> string, finalize: unit -> string}
-  val register_action: string -> (action_context -> action) -> unit
+  val register_action: string -> (action_context -> string * action) -> unit
 
   (*utility functions*)
   val print_exn: exn -> string
@@ -71,7 +71,7 @@
 
 local
   val actions = Synchronized.var "Mirabelle.actions"
-    (Symtab.empty : (action_context -> action) Symtab.table);
+    (Symtab.empty : (action_context -> string * action) Symtab.table);
 in
 
 fun register_action name make_action =
@@ -100,6 +100,21 @@
 fun make_action_path ({index, label, name, ...} : action_context) =
   Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);
 
+fun initialize_action (make_action : action_context -> string * action) context =
+  let
+    val (s, action) = make_action context
+    val action_path = make_action_path context;
+    val export_name =
+      Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "initialize");
+    val () =
+      if s <> "" then
+        Export.export \<^theory> export_name [XML.Text s]
+      else
+        ()
+  in
+    action
+  end
+
 fun finalize_action ({finalize, ...} : action) context =
   let
     val s = run_action_function finalize;
@@ -232,7 +247,7 @@
                 {index = n, label = label, name = name, arguments = args,
                  timeout = mirabelle_timeout, output_dir = output_dir};
             in
-              (make_action context, context)
+              (initialize_action make_action context, context)
             end);
         in
           (* run actions on all relevant goals *)
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun Dec 19 11:15:21 2021 +0100
@@ -85,7 +85,8 @@
                   val lines = Pretty.string_of(yxml).trim()
                   val prefix =
                     Export.explode_name(args.name) match {
-                      case List("mirabelle", action, "finalize") => action + " finalize  "
+                      case List("mirabelle", action, "initialize") => action + " initialize "
+                      case List("mirabelle", action, "finalize") => action + " finalize   "
                       case List("mirabelle", action, "goal", goal_name, line, offset) =>
                         action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " +
                           line + ":" + offset + "  "
--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -16,7 +16,7 @@
       (case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
         ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
       | (_, false) => "failed")
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "arith" make_action
 
--- a/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_metis.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -21,7 +21,7 @@
         (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
         |> not (null names) ? suffix (":\n" ^ commas names)
       end
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "metis" make_action
 
--- a/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -14,7 +14,7 @@
       (case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
         ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
       | (_, false) => "failed")
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "presburger" make_action
 
--- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -19,7 +19,7 @@
       (case Timeout.apply timeout quickcheck pre of
         NONE => "no counterexample"
       | SOME _ => "counterexample found")
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "quickcheck" make_action
 
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -24,7 +24,6 @@
 val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*)
 val keepK = "keep" (*=BOOL: keep temporary files created by sledgehammer*)
 val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*)
-val proverK = "prover" (*=STRING: name of the external prover to call*)
 val term_orderK = "term_order" (*=STRING: term order (in E)*)
 
 (*defaults used in this Mirabelle action*)
@@ -39,8 +38,7 @@
   lemmas: int,
   max_lems: int,
   time_isa: int,
-  time_prover: int,
-  time_prover_fail: int}
+  time_prover: int}
 
 datatype re_data = ReData of {
   calls: int,
@@ -56,11 +54,10 @@
 
 fun make_sh_data
       (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,
-       time_prover,time_prover_fail) =
+       time_prover) =
   ShData{calls=calls, success=success, nontriv_calls=nontriv_calls,
          nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,
-         time_isa=time_isa, time_prover=time_prover,
-         time_prover_fail=time_prover_fail}
+         time_isa=time_isa, time_prover=time_prover}
 
 fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
                   timeout,lemmas,posns) =
@@ -68,13 +65,12 @@
          nontriv_success=nontriv_success, proofs=proofs, time=time,
          timeout=timeout, lemmas=lemmas, posns=posns}
 
-val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0)
+val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0)
 val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])
 
-fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
-                              lemmas, max_lems, time_isa,
-  time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
-  nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)
+fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems,
+    time_isa, time_prover}) =
+  (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover)
 
 fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success,
   proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
@@ -104,40 +100,37 @@
 fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
 
 val inc_sh_calls =  map_sh_data
-  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
-    => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) =>
+    (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover))
 
 val inc_sh_success = map_sh_data
-  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
-    => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) =>
+    (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover))
 
 val inc_sh_nontriv_calls =  map_sh_data
-  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
-    => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) =>
+    (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover))
 
 val inc_sh_nontriv_success = map_sh_data
-  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
-    => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover) =>
+    (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover))
 
 fun inc_sh_lemmas n = map_sh_data
-  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
-    => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) =>
+    (calls, success, nontriv_calls, nontriv_success, lemmas+n, max_lems, time_isa, time_prover))
 
 fun inc_sh_max_lems n = map_sh_data
-  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
-    => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) =>
+    (calls, success,nontriv_calls, nontriv_success, lemmas, Int.max (max_lems, n), time_isa,
+     time_prover))
 
 fun inc_sh_time_isa t = map_sh_data
-  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
-    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) =>
+    (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa + t, time_prover))
 
 fun inc_sh_time_prover t = map_sh_data
-  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
-    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail))
-
-fun inc_sh_time_prover_fail t = map_sh_data
-  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
-    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))
+  (fn (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover) =>
+    (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover + t))
 
 val inc_proof_method_calls = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
@@ -187,7 +180,7 @@
   if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
 
 fun log_sh_data (ShData {calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa,
-      time_prover, time_prover_fail}) =
+      time_prover}) =
   "\nTotal number of sledgehammer calls: " ^ str calls ^
   "\nNumber of successful sledgehammer calls: " ^ str success ^
   "\nNumber of sledgehammer lemmas: " ^ str lemmas ^
@@ -197,13 +190,10 @@
   "\nNumber of successful nontrivial sledgehammer calls: " ^ str nontriv_success ^
   "\nTotal time for sledgehammer calls (Isabelle): " ^ str3 (ms time_isa) ^
   "\nTotal time for successful sledgehammer calls (ATP): " ^ str3 (ms time_prover) ^
-  "\nTotal time for failed sledgehammer calls (ATP): " ^ str3 (ms time_prover_fail) ^
   "\nAverage time for sledgehammer calls (Isabelle): " ^
     str3 (avg_time time_isa calls) ^
   "\nAverage time for successful sledgehammer calls (ATP): " ^
-    str3 (avg_time time_prover success) ^
-  "\nAverage time for failed sledgehammer calls (ATP): " ^
-    str3 (avg_time time_prover_fail (calls - success))
+    str3 (avg_time time_prover success)
 
 fun log_re_data sh_calls (ReData {calls, success, nontriv_calls, nontriv_success, proofs, time,
       timeout, lemmas = (lemmas, lems_sos, lems_max), posns}) =
@@ -246,24 +236,6 @@
 
 end
 
-fun get_prover_name thy args =
-  let
-    fun default_prover_name () =
-      hd (#provers (Sledgehammer_Commands.default_params thy []))
-      handle List.Empty => error "No ATP available"
-  in
-    (case AList.lookup (op =) args proverK of
-      SOME name => name
-    | NONE => default_prover_name ())
-  end
-
-fun get_prover ctxt name params goal =
-  let
-    val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal)
-  in
-    Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name
-  end
-
 type stature = ATP_Problem_Generate.stature
 
 fun is_good_line s =
@@ -299,17 +271,8 @@
 
 local
 
-datatype sh_result =
-  SH_OK of int * int * (string * stature) list |
-  SH_FAIL of int * int |
-  SH_ERROR
-
-fun run_sh (params as {max_facts, minimize, preplay_timeout, ...}) prover_name e_selection_heuristic
-    term_order force_sos hard_timeout dir pos st =
+fun run_sh params e_selection_heuristic term_order force_sos dir pos state =
   let
-    val thy = Proof.theory_of st
-    val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
-    val i = 1
     fun set_file_name (SOME dir) =
         let
           val filename = "prob_" ^
@@ -321,8 +284,8 @@
           #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
         end
       | set_file_name NONE = I
-    val st' =
-      st
+    val state' =
+      state
       |> Proof.map_context
            (set_file_name dir
             #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic)
@@ -331,57 +294,20 @@
                   term_order |> the_default I)
             #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos)
                   force_sos |> the_default I))
-    val default_max_facts =
-      Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
-    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
-    val time_limit =
-      (case hard_timeout of
-        NONE => I
-      | SOME t => Timeout.apply t)
-    fun failed failure =
-      ({outcome = SOME failure, used_facts = [], used_from = [],
-        preferred_methss = (Sledgehammer_Proof_Methods.Auto_Method, []), run_time = Time.zeroTime,
-        message = K ""}, ~1)
-    val ({outcome, used_facts, preferred_methss, run_time, message, ...}
-         : Sledgehammer_Prover.prover_result,
-         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
-      let
-        val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name
-        val keywords = Thy_Header.get_keywords' ctxt
-        val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-        val facts =
-          Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
-              Sledgehammer_Fact.no_fact_override keywords css_table chained_ths
-              hyp_ts concl_t
-        val factss =
-          facts
-          |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
-                 (the_default default_max_facts max_facts)
-                 Sledgehammer_Fact.no_fact_override hyp_ts concl_t
-          |> tap (fn factss =>
-                     "Line " ^ str0 (Position.line_of pos) ^ ": " ^
-                     Sledgehammer.string_of_factss factss
-                     |> writeln)
-        val prover = get_prover ctxt prover_name params goal
-        val problem =
-          {comment = "", state = st', goal = goal, subgoal = i,
-           subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I}
-      in prover params problem end)) ()
-      handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut
-           | Fail "inappropriate" => failed ATP_Proof.Inappropriate
-    val time_prover = run_time |> Time.toMilliseconds
-    val msg = message (fn () => Sledgehammer.play_one_line_proof minimize preplay_timeout used_facts
-      st' i preferred_methss)
+
+    val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
+      Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
+        Sledgehammer_Fact.no_fact_override state') ()
   in
-    (case outcome of
-      NONE => (msg, SH_OK (time_isa, time_prover, used_facts))
-    | SOME _ => (msg, SH_FAIL (time_isa, time_prover)))
+    (sledgehammer_outcome, msg, cpu_time)
   end
-  handle ERROR msg => ("error: " ^ msg, SH_ERROR)
+  handle
+    ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
+  | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
 
 in
 
-fun run_sledgehammer change_data (params as {provers, timeout, ...}) output_dir
+fun run_sledgehammer change_data (params as {provers, ...}) output_dir
   e_selection_heuristic term_order force_sos keep proof_method_from_msg thy_index trivial
   proof_method named_thms pos st =
   let
@@ -400,17 +326,15 @@
         end
       else
         NONE
-    (* always use a hard timeout, but give some slack so that the automatic
-       minimizer has a chance to do its magic *)
-    val hard_timeout = SOME (Time.scale 4.0 timeout)
     val prover_name = hd provers
-    val (msg, result) =
-      run_sh params prover_name e_selection_heuristic term_order force_sos hard_timeout keep_dir pos
-        st
-  in
-    (case result of
-      SH_OK (time_isa, time_prover, names) =>
+    val (sledgehamer_outcome, msg, cpu_time) =
+      run_sh params e_selection_heuristic term_order force_sos keep_dir pos st
+    val outcome_msg =
+      (case sledgehamer_outcome of
+        Sledgehammer.SH_Some {used_facts, run_time, ...} =>
         let
+          val num_used_facts = length used_facts
+          val time_prover = Time.toMilliseconds run_time
           fun get_thms (name, stature) =
             try (Sledgehammer_Util.thms_of_name (Proof.context_of st))
               name
@@ -418,21 +342,19 @@
         in
           change_data inc_sh_success;
           if trivial then () else change_data inc_sh_nontriv_success;
-          change_data (inc_sh_lemmas (length names));
-          change_data (inc_sh_max_lems (length names));
-          change_data (inc_sh_time_isa time_isa);
+          change_data (inc_sh_lemmas num_used_facts);
+          change_data (inc_sh_max_lems num_used_facts);
           change_data (inc_sh_time_prover time_prover);
           proof_method := proof_method_from_msg msg;
-          named_thms := SOME (map_filter get_thms names);
-          triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
-            string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg
+          named_thms := SOME (map_filter get_thms used_facts);
+          " (" ^ string_of_int cpu_time ^ "+" ^ string_of_int time_prover ^ ")" ^
+          " [" ^ prover_name ^ "]:\n"
         end
-    | SH_FAIL (time_isa, time_prover) =>
-        let
-          val _ = change_data (inc_sh_time_isa time_isa)
-          val _ = change_data (inc_sh_time_prover_fail time_prover)
-        in triv_str ^ "failed: " ^ msg end
-    | SH_ERROR => "failed: " ^ msg)
+      | _ => "")
+  in
+    change_data (inc_sh_time_isa cpu_time);
+    Sledgehammer.short_string_of_sledgehammer_outcome sledgehamer_outcome ^ " " ^
+      triv_str ^ outcome_msg ^ msg
   end
 
 end
@@ -531,11 +453,13 @@
       |> (fn (params as {provers, ...}) =>
             (case provers of
               prover :: _ => Sledgehammer_Prover.set_params_provers params [prover]
-            | _ => error "sledgehammer action requires one prover"))
+            | _ => error "sledgehammer action requires one and only one prover"))
 
     val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data
     val change_data = Synchronized.change data
 
+    val init_msg = "Params for sledgehammer: " ^ Sledgehammer_Prover.string_of_params params
+
     fun run_action ({theory_index, name, pos, pre, ...} : Mirabelle.command) =
       let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
         if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal then
@@ -561,8 +485,8 @@
       end
 
     fun finalize () = log_data (Synchronized.value data)
-  in {run_action = run_action, finalize = finalize} end
+  in (init_msg, {run_action = run_action, finalize = finalize}) end
 
 val () = Mirabelle.register_action "sledgehammer" make_action
 
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -179,7 +179,7 @@
             (Synchronized.value num_lost_facts) ^ "%"
       else
         ""
-  in {run_action = run_action, finalize = finalize} end
+  in ("", {run_action = run_action, finalize = finalize}) end
 
 val () = Mirabelle.register_action "sledgehammer_filter" make_action
 
--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -18,7 +18,7 @@
         "succeeded"
       else
         ""
-  in {run_action = run_action, finalize = K ""} end
+  in ("", {run_action = run_action, finalize = K ""}) end
 
 val () = Mirabelle.register_action "try0" make_action
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -15,17 +15,21 @@
   type play_outcome = Sledgehammer_Proof_Methods.play_outcome
   type mode = Sledgehammer_Prover.mode
   type params = Sledgehammer_Prover.params
+  type induction_rules = Sledgehammer_Prover.induction_rules
+  type prover_problem = Sledgehammer_Prover.prover_problem
+  type prover_result = Sledgehammer_Prover.prover_result
 
-  val someN : string
-  val noneN : string
-  val timeoutN : string
-  val unknownN : string
+  datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None
 
+  val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string
+
+  val induction_rules_for_prover : Proof.context -> string -> induction_rules option ->
+    induction_rules
   val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int ->
     proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome)
   val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
-    Proof.state -> bool * (string * string list)
+    Proof.state -> bool * (sledgehammer_outcome * string)
 end;
 
 structure Sledgehammer : SLEDGEHAMMER =
@@ -45,20 +49,37 @@
 open Sledgehammer_Prover_Minimize
 open Sledgehammer_MaSh
 
-val someN = "some"
-val noneN = "none"
-val timeoutN = "timeout"
-val unknownN = "unknown"
+datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None
+
+fun is_sledgehammer_outcome_some (SH_Some _) = true
+  | is_sledgehammer_outcome_some _ = false
 
-val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
+fun short_string_of_sledgehammer_outcome (SH_Some _) = "some"
+  | short_string_of_sledgehammer_outcome SH_Unknown = "unknown"
+  | short_string_of_sledgehammer_outcome SH_Timeout = "timeout"
+  | short_string_of_sledgehammer_outcome SH_None = "none"
+
+fun alternative f (SOME x) (SOME y) = SOME (f (x, y))
+  | alternative _ (x as SOME _) NONE = x
+  | alternative _ NONE (y as SOME _) = y
+  | alternative _ NONE NONE = NONE
 
-fun max_outcome_code codes =
-  NONE
-  |> fold (fn candidate =>
-      fn accum as SOME _ => accum
-       | NONE => if member (op =) codes candidate then SOME candidate else NONE)
-    ordered_outcome_codes
-  |> the_default unknownN
+fun max_outcome outcomes =
+  let
+    val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes
+    val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes
+    val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes
+    val none = find_first (fn (SH_None, _) => true | _ => false) outcomes
+  in
+    some
+    |> alternative snd unknown
+    |> alternative snd timeout
+    |> alternative snd none
+    |> the_default (SH_Unknown, "")
+  end
+
+fun induction_rules_for_prover ctxt prover_name induction_rules =
+  the_default (if is_ho_atp ctxt prover_name then Include else Exclude) induction_rules
 
 fun is_metis_method (Metis_Method _) = true
   | is_metis_method _ = false
@@ -115,26 +136,25 @@
   |> (fn (used_facts, (meth, play)) =>
         (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
 
-fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
-      expect, induction_rules, ...}) mode writeln_result only learn
-    {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name =
+fun launch_prover (params as {verbose, spy, max_facts, induction_rules, ...}) mode only learn
+    ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) name =
   let
     val ctxt = Proof.context_of state
 
-    val hard_timeout = Time.scale 5.0 timeout
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
-    val num_facts = length facts |> not only ? Integer.min max_facts
-    val induction_rules =
-      the_default (if is_ho_atp ctxt name then Include else Exclude) induction_rules
+    val num_facts =
+      (case factss of
+        (_, facts) :: _ => length facts |> not only ? Integer.min max_facts
+      | _ => 0)
+    val induction_rules = induction_rules_for_prover ctxt name induction_rules
 
     val problem =
       {comment = comment, state = state, goal = goal, subgoal = subgoal,
        subgoal_count = subgoal_count,
        factss = factss
-       |> map (apsnd ((induction_rules = Exclude
-           ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false))
-         #> take num_facts)),
+         (* We take num_facts because factss contains the maximum of all called provers. *)
+         |> map (apsnd (take num_facts o maybe_filter_out_induction_rules induction_rules)),
        found_proof = found_proof}
 
     fun print_used_facts used_facts used_from =
@@ -143,8 +163,8 @@
       |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
-      |> prefix ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
-        " proof (of " ^ string_of_int (length facts) ^ "): ")
+      |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ quote name ^
+        " proof (of " ^ string_of_int num_facts ^ "): ")
       |> writeln
 
     fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
@@ -178,58 +198,77 @@
         end
       | spying_str_of_res {outcome = SOME failure, ...} =
         "Failure: " ^ string_of_atp_failure failure
+ in
+  problem
+  |> get_minimizing_prover ctxt mode learn name params
+  |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
+      print_used_facts used_facts used_from
+    | _ => ())
+  |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
+ end
+
+fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal
+    (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
+  let
+    val output =
+      if outcome = SOME ATP_Proof.TimedOut then
+        SH_Timeout
+      else if is_some outcome then
+        SH_None
+      else
+        SH_Some result
+    fun output_message () = message (fn () =>
+      play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss)
+  in
+    (output, output_message)
+  end
+
+fun check_expected_outcome ctxt prover_name expect outcome =
+  let
+    val outcome_code = short_string_of_sledgehammer_outcome outcome
+  in
+    (* The "expect" argument is deliberately ignored if the prover is
+       missing so that the "Metis_Examples" can be processed on any
+       machine. *)
+    if expect = "" orelse outcome_code = expect orelse
+       not (is_prover_installed ctxt prover_name) then
+      ()
+    else
+      error ("Unexpected outcome: " ^ quote outcome_code)
+  end
+
+fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result only
+    learn (problem as {state, subgoal, ...}) prover_name =
+  let
+    val ctxt = Proof.context_of state
+    val hard_timeout = Time.scale 5.0 timeout
 
     fun really_go () =
-      problem
-      |> get_minimizing_prover ctxt mode learn name params
-      |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
-          print_used_facts used_facts used_from
-        | _ => ())
-      |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
-      |> (fn {outcome, used_facts, preferred_methss, message, ...} =>
-        (if outcome = SOME ATP_Proof.TimedOut then timeoutN
-         else if is_some outcome then noneN
-         else someN,
-         fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state
-           subgoal preferred_methss)))
+      launch_prover params mode only learn problem prover_name
+      |> preplay_prover_result params state subgoal
 
     fun go () =
-      let
-        val (outcome_code, message) =
-          if debug then
-            really_go ()
-          else
-            (really_go ()
-             handle
-               ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
-             | exn =>
-               if Exn.is_interrupt exn then Exn.reraise exn
-               else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
+      if debug then
+        really_go ()
+      else
+        (really_go ()
+         handle
+           ERROR msg => (SH_Unknown, fn () => "Error: " ^ msg ^ "\n")
+         | exn =>
+           if Exn.is_interrupt exn then Exn.reraise exn
+           else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
 
-        val _ =
-          (* The "expect" argument is deliberately ignored if the prover is
-             missing so that the "Metis_Examples" can be processed on any
-             machine. *)
-          if expect = "" orelse outcome_code = expect orelse
-             not (is_prover_installed ctxt name) then
-            ()
-          else
-            error ("Unexpected outcome: " ^ quote outcome_code)
-      in (outcome_code, message) end
+    val (outcome, message) = Timeout.apply hard_timeout go ()
+    val () = check_expected_outcome ctxt prover_name expect outcome
+
+    val message = message ()
+    val () =
+      if mode <> Auto_Try andalso is_sledgehammer_outcome_some outcome orelse mode = Normal then
+        the_default writeln writeln_result (quote prover_name ^ ": " ^ message)
+      else
+        ()
   in
-    if mode = Auto_Try then
-      let val (outcome_code, message) = Timeout.apply timeout go () in
-        (outcome_code, if outcome_code = someN then [message ()] else [])
-      end
-    else
-      let
-        val (outcome_code, message) = Timeout.apply hard_timeout go ()
-        val outcome =
-          if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
-        val _ =
-          if outcome <> "" andalso is_some writeln_result then the writeln_result outcome
-          else writeln outcome
-      in (outcome_code, []) end
+    (outcome, message)
   end
 
 val auto_try_max_facts_divisor = 2 (* FUDGE *)
@@ -251,7 +290,7 @@
     error "No prover is set"
   else
     (case subgoal_count state of
-      0 => (error "No subgoal!"; (false, (noneN, [])))
+      0 => (error "No subgoal!"; (false, (SH_None, "")))
     | n =>
       let
         val _ = Proof.assert_backward state
@@ -268,13 +307,11 @@
             I
 
         val ctxt = Proof.context_of state
-        val keywords = Thy_Header.get_keywords' ctxt
-        val {facts = chained, goal, ...} = Proof.goal state
+        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 inst_inducts = induction_rules = SOME Instantiate
-        val css = clasimpset_rule_table_of ctxt
         val all_facts =
-          nearly_all_facts ctxt inst_inducts fact_override keywords css chained hyp_ts concl_t
+          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)
@@ -311,24 +348,23 @@
               {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
                factss = factss, found_proof = found_proof}
             val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
-            val launch = launch_prover params mode writeln_result only learn
+            val launch = launch_prover_and_preplay params mode writeln_result only learn
           in
             if mode = Auto_Try then
-              (unknownN, [])
-              |> fold (fn prover => fn accum as (outcome_code, _) =>
-                  if outcome_code = someN then accum else launch problem prover)
+              (SH_Unknown, "")
+              |> fold (fn prover => fn accum as (SH_Some _, _) => accum | _ => launch problem prover)
                 provers
             else
-              (learn chained;
+              (learn chained_thms;
                provers
-               |> Par_List.map (launch problem #> fst)
-               |> max_outcome_code |> rpair [])
+               |> Par_List.map (launch problem)
+               |> max_outcome)
           end
       in
         launch_provers ()
         handle Timeout.TIMEOUT _ =>
-          (print "Sledgehammer ran out of time"; (unknownN, []))
+          (print "Sledgehammer ran out of time"; (SH_Timeout, ""))
       end
-      |> `(fn (outcome_code, _) => outcome_code = someN))
+      |> `(fn (outcome, _) => is_sledgehammer_outcome_some outcome))
 
 end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -384,7 +384,7 @@
    prem_role = Hypothesis,
    best_slices =
      (* FUDGE *)
-     K [(1.0, (((150, ""), THF (Polymorphic, {with_ite = true, with_let = true}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), ""))],
+     K [(1.0, (((512, ""), TH1, "mono_native_higher", keep_lamsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    best_max_new_mono_instances = default_max_new_mono_instances}
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -394,6 +394,7 @@
         val i = 1
       in
         run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state)
+        |> apsnd (map_prod short_string_of_sledgehammer_outcome single)
       end}
 
 val _ =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -37,6 +37,8 @@
     status Termtab.table -> lazy_fact list
   val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords ->
     status Termtab.table -> thm list -> term list -> term -> lazy_fact list
+  val nearly_all_facts_of_context : Proof.context -> bool -> fact_override -> thm list ->
+    term list -> term -> lazy_fact list
   val drop_duplicate_facts : lazy_fact list -> lazy_fact list
 end;
 
@@ -554,6 +556,14 @@
       |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t
     end
 
+fun nearly_all_facts_of_context ctxt inst_inducts fact_override =
+  let
+    val keywords = Thy_Header.get_keywords' ctxt
+    val css = clasimpset_rule_table_of ctxt
+  in
+    nearly_all_facts ctxt inst_inducts fact_override keywords css
+  end
+
 fun drop_duplicate_facts facts =
   let val num_facts = length facts in
     facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Dec 17 16:36:42 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Sun Dec 19 11:15:21 2021 +0100
@@ -19,6 +19,7 @@
 
   datatype induction_rules = Include | Exclude | Instantiate
   val induction_rules_of_string : string -> induction_rules option
+  val maybe_filter_out_induction_rules : induction_rules -> fact list -> fact list
 
   type params =
     {debug : bool,
@@ -47,6 +48,7 @@
      preplay_timeout : Time.time,
      expect : string}
 
+  val string_of_params : params -> string
   val set_params_provers : params -> string list -> params
 
   type prover_problem =
@@ -143,6 +145,13 @@
    preplay_timeout : Time.time,
    expect : string}
 
+fun string_of_params (params : params) =
+  YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100)))
+
+fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
+    induction_rules = Exclude ?
+      filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
+
 fun set_params_provers params provers =
   {debug = #debug params,
    verbose = #verbose params,