# HG changeset patch # User paulson # Date 1743781096 -3600 # Node ID 13a185b64ffff8bd49fe8e811244008ae7f978b9 # Parent 9d457dfb56c5175a5e31722eb4ed91bc650603e3# Parent 24d09a911713f1678ee252b94989ae1772e61596 merged diff -r 24d09a911713 -r 13a185b64fff NEWS --- a/NEWS Fri Apr 04 16:37:58 2025 +0100 +++ b/NEWS Fri Apr 04 16:38:16 2025 +0100 @@ -35,15 +35,15 @@ * Theory "HOL.Fun": - Added lemmas. - mono_on_strict_invE - mono_on_invE - strict_mono_on_eq - strict_mono_on_less_eq - strict_mono_on_less antimonotone_on_inf_fun antimonotone_on_sup_fun + mono_on_invE + mono_on_strict_invE monotone_on_inf_fun monotone_on_sup_fun + strict_mono_on_eq + strict_mono_on_less + strict_mono_on_less_eq - Removed lemmas. Minor INCOMPATIBILITY. mono_on_greaterD (use mono_invE instead) diff -r 24d09a911713 -r 13a185b64fff src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Apr 04 16:37:58 2025 +0100 +++ b/src/HOL/Sledgehammer.thy Fri Apr 04 16:38:16 2025 +0100 @@ -7,7 +7,15 @@ section \Sledgehammer: Isabelle--ATP Linkup\ theory Sledgehammer -imports Presburger SMT Try0_HOL + imports + \ \FIXME: \<^theory>\HOL.Try0_HOL\ 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>\HOL.Try0\, + which is imported transitively by both \<^theory>\HOL.Presburger\ and \<^theory>\HOL.SMT\. It seems + that, when merging the attributes from two theories, the value assigned int the leftmost theory + has precedence.\ + Try0_HOL + Presburger + SMT keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl diff -r 24d09a911713 -r 13a185b64fff src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Fri Apr 04 16:37:58 2025 +0100 +++ b/src/HOL/Tools/try0.ML Fri Apr 04 16:38:16 2025 +0100 @@ -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 @@ -111,7 +107,7 @@ fun get_proof_method_or_noop name = (case get_proof_method name of - NONE => noop_proof_method + NONE => (warning ("Proof method \"" ^ name ^ "\" is undefined"); noop_proof_method) | SOME proof_method => proof_method) fun maybe_apply_proof_method name mode : proof_method = @@ -120,10 +116,15 @@ else noop_proof_method +val schedule = Attrib.setup_config_string \<^binding>\try0_schedule\ (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 24d09a911713 -r 13a185b64fff src/HOL/Try0_HOL.thy --- a/src/HOL/Try0_HOL.thy Fri Apr 04 16:37:58 2025 +0100 +++ b/src/HOL/Try0_HOL.thy Fri Apr 04 16:38:16 2025 +0100 @@ -43,6 +43,7 @@ ("force", (false, (false, full_attrs))), ("meson", (false, (false, metis_attrs))), ("satx", (false, (false, no_attrs))), + ("iprover", (false, (false, no_attrs))), ("order", (true, (false, no_attrs)))] in @@ -62,4 +63,10 @@ end \ +declare [[try0_schedule = " + satx iprover metis | + order presburger linarith algebra argo | + simp auto blast fast fastforce force meson +"]] + end \ No newline at end of file