# HG changeset patch
# User desharna
# Date 1743585515 -7200
# Node ID 7230281bde03cab8ee92a0400aa8fc38284f4120
# Parent  88064da0ae76ac6f98fd3e77585c0b7189a6e166
added a user-configurable schedule to try0

diff -r 88064da0ae76 -r 7230281bde03 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Apr 01 12:10:45 2025 +0200
+++ b/src/HOL/Sledgehammer.thy	Wed Apr 02 11:18:35 2025 +0200
@@ -7,7 +7,15 @@
 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
 
 theory Sledgehammer
-imports Presburger SMT Try0_HOL
+  imports
+    \<comment> \<open>FIXME: \<^theory>\<open>HOL.Try0_HOL\<close> has to be imported first so that @{attribute try0_schedule} gets
+    the value assigned value there. Otherwise, the value is the one assigned in \<^theory>\<open>HOL.Try0\<close>,
+    which is imported transitively by both \<^theory>\<open>HOL.Presburger\<close> and \<^theory>\<open>HOL.SMT\<close>. It seems
+    that, when merging the attributes from two theories, the value assigned int the leftmost theory
+    has precedence.\<close>
+    Try0_HOL
+    Presburger
+    SMT
 keywords
   "sledgehammer" :: diag and
   "sledgehammer_params" :: thy_decl
diff -r 88064da0ae76 -r 7230281bde03 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Tue Apr 01 12:10:45 2025 +0200
+++ b/src/HOL/Tools/try0.ML	Wed Apr 02 11:18:35 2025 +0200
@@ -29,6 +29,8 @@
   val get_proof_method_or_noop : string -> proof_method
   val get_all_proof_method_names : unit -> string list
 
+  val schedule : string Config.T
+
   datatype mode = Auto_Try | Try | Normal
   val generic_try0 : mode -> Time.time option -> facts -> Proof.state ->
     (bool * (string * string list)) * result list
@@ -95,15 +97,9 @@
 fun get_proof_method (name : string) : proof_method option =
   Symtab.lookup (Synchronized.value proof_methods) name;
 
-fun get_all_proof_methods () : (string * proof_method) list =
-  Symtab.fold (fn x => fn xs => x :: xs) (Synchronized.value proof_methods) []
-
 fun get_all_proof_method_names () : string list =
   Symtab.fold (fn (name, _) => fn names => name :: names) (Synchronized.value proof_methods) []
 
-fun get_all_auto_try_proof_method_names () : string list =
-  Symset.dest (Synchronized.value auto_try_proof_methods_names)
-
 fun should_auto_try_proof_method (name : string) : bool =
   Symset.member (Synchronized.value auto_try_proof_methods_names) name
 
@@ -120,10 +116,15 @@
   else
     noop_proof_method
 
+val schedule = Attrib.setup_config_string \<^binding>\<open>try0_schedule\<close> (K "")
+
+local
+
 fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
 fun tool_time_string (s, time) = s ^ ": " ^ time_string time
 
-fun generic_try0 mode timeout_opt (facts : facts) st =
+fun generic_try0_step mode (timeout_opt : Time.time option) (facts : facts) (st : Proof.state)
+  (proof_methods : string list) =
   let
     fun try_method (method : mode -> proof_method) = method mode timeout_opt facts st
     fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command
@@ -139,11 +140,10 @@
         methods
         |> Par_List.get_some try_method
         |> the_list
-    val proof_method_names = get_all_proof_method_names ()
-    val maybe_apply_methods = map maybe_apply_proof_method proof_method_names
+    val maybe_apply_methods = map maybe_apply_proof_method proof_methods
   in
     if mode = Normal then
-      let val names = map quote proof_method_names in
+      let val names = map quote proof_methods in
         writeln ("Trying " ^ implode_space (serial_commas "and" names) ^ "...")
       end
     else
@@ -171,6 +171,31 @@
       end)
   end
 
+in
+
+fun generic_try0 mode (timeout_opt : Time.time option) (facts : facts) (st : Proof.state) =
+  let
+    fun some_nonempty_string sub =
+      if Substring.isEmpty sub then
+        NONE
+      else
+        SOME (Substring.string sub)
+    val schedule =
+      Config.get (Proof.context_of st) schedule
+      |> Substring.full
+      |> Substring.tokens (fn c => c = #"|")
+      |> map (map_filter some_nonempty_string o Substring.tokens Char.isSpace)
+    fun iterate [] = ((false, (noneN, [])), [])
+      | iterate (proof_methods :: proof_methodss) =
+        (case generic_try0_step mode timeout_opt facts st proof_methods of
+          (_, []) => iterate proof_methodss
+        | result as (_, _ :: _) => result)
+  in
+    iterate (if null schedule then [get_all_proof_method_names ()] else schedule)
+  end;
+
+end
+
 fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt
 
 fun try0_trans (facts : facts) =
diff -r 88064da0ae76 -r 7230281bde03 src/HOL/Try0_HOL.thy
--- a/src/HOL/Try0_HOL.thy	Tue Apr 01 12:10:45 2025 +0200
+++ b/src/HOL/Try0_HOL.thy	Wed Apr 02 11:18:35 2025 +0200
@@ -62,4 +62,10 @@
 end
 \<close>
 
+declare [[try0_schedule = "
+  satx metis |
+  order presburger linarith algebra argo |
+  simp auto blast fast fastforce force meson
+"]]
+
 end
\ No newline at end of file