# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 340187063d847d3d409ff5e00bf2d7c7d108d28c # Parent 325c8fd0d7620f7f16859db57dc221a6b47a6f51 use async manager to manage MaSh learners to make sure they get killed cleanly diff -r 325c8fd0d762 -r 340187063d84 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Jul 18 08:44:04 2012 +0200 @@ -8,12 +8,12 @@ signature ASYNC_MANAGER = sig - val implode_desc : string * string -> string val break_into_chunks : string -> string list val launch : string -> Time.time -> Time.time -> string * string -> (unit -> bool * string) -> unit val kill_threads : string -> string -> unit + val has_running_threads : string -> bool val running_threads : string -> string -> unit val thread_messages : string -> string -> int option -> unit end; @@ -23,29 +23,27 @@ (** preferences **) -val message_store_limit = 20; -val message_display_limit = 10; +val message_store_limit = 20 +val message_display_limit = 10 (** thread management **) -val implode_desc = op ^ o apfst quote - fun implode_message (workers, work) = - space_implode " " (Try.serial_commas "and" (map quote workers)) ^ work + space_implode " " (Try.serial_commas "and" workers) ^ work (* data structures over threads *) structure Thread_Heap = Heap ( - type elem = Time.time * Thread.thread; - fun ord ((a, _), (b, _)) = Time.compare (a, b); -); + type elem = Time.time * Thread.thread + fun ord ((a, _), (b, _)) = Time.compare (a, b) +) -fun lookup_thread xs = AList.lookup Thread.equal xs; -fun delete_thread xs = AList.delete Thread.equal xs; -fun update_thread xs = AList.update Thread.equal xs; +fun lookup_thread xs = AList.lookup Thread.equal xs +fun delete_thread xs = AList.delete Thread.equal xs +fun update_thread xs = AList.update Thread.equal xs (* state of thread manager *) @@ -65,7 +63,7 @@ canceling = canceling, messages = messages, store = store} val global_state = Synchronized.var "async_manager" - (make_state NONE Thread_Heap.empty [] [] [] []); + (make_state NONE Thread_Heap.empty [] [] [] []) (* unregister thread *) @@ -76,22 +74,23 @@ (case lookup_thread active thread of SOME (tool, _, _, desc as (worker, its_desc)) => let - val active' = delete_thread thread active; + val active' = delete_thread thread active val now = Time.now () val canceling' = (thread, (tool, now, desc)) :: canceling - val message' = (worker, its_desc ^ "\n" ^ message) + val message' = + (worker, its_desc ^ (if message = "" then "" else "\n" ^ message)) val messages' = (urgent, (tool, message')) :: messages val store' = (tool, message') :: (if length store <= message_store_limit then store - else #1 (chop message_store_limit store)); + else #1 (chop message_store_limit store)) in make_state manager timeout_heap active' canceling' messages' store' end - | NONE => state)); + | NONE => state)) (* main manager thread -- only one may exist *) -val min_wait_time = seconds 0.3; -val max_wait_time = seconds 10.0; +val min_wait_time = seconds 0.3 +val max_wait_time = seconds 10.0 fun replace_all bef aft = let @@ -119,7 +118,8 @@ postponed_messages store)) |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker)) |> AList.group (op =) - |> List.app (fn ((tool, work), workers) => + |> List.app (fn ((_, ""), _) => () + | ((tool, work), workers) => tool ^ ": " ^ implode_message (workers |> sort_distinct string_ord, work) |> break_into_chunks @@ -133,12 +133,12 @@ fun time_limit timeout_heap = (case try Thread_Heap.min timeout_heap of NONE => Time.+ (Time.now (), max_wait_time) - | SOME (time, _) => time); + | SOME (time, _) => time) (*action: find threads whose timeout is reached, and interrupt canceling threads*) fun action {manager, timeout_heap, active, canceling, messages, store} = let val (timeout_threads, timeout_heap') = - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap; + Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap in if null timeout_threads andalso null canceling then NONE @@ -146,9 +146,9 @@ let val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling val canceling' = filter (Thread.isActive o #1) canceling - val state' = make_state manager timeout_heap' active canceling' messages store; + val state' = make_state manager timeout_heap' active canceling' messages store in SOME (map #2 timeout_threads, state') end - end; + end in while Synchronized.change_result global_state (fn state as {timeout_heap, active, canceling, messages, store, ...} => @@ -156,12 +156,13 @@ then (false, make_state NONE timeout_heap active canceling messages store) else (true, state)) do - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action - |> these - |> List.app (unregister (false, "Timed out.")); - print_new_messages (); - (*give threads some time to respond to interrupt*) - OS.Process.sleep min_wait_time) + (Synchronized.timed_access global_state + (SOME o time_limit o #timeout_heap) action + |> these + |> List.app (unregister (false, "Timed out.")); + print_new_messages (); + (* give threads some time to respond to interrupt *) + OS.Process.sleep min_wait_time) end)) in make_state manager timeout_heap active canceling messages store end) @@ -172,9 +173,9 @@ (Synchronized.change global_state (fn {manager, timeout_heap, active, canceling, messages, store} => let - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap; - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active; - val state' = make_state manager timeout_heap' active' canceling messages store; + val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap + val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active + val state' = make_state manager timeout_heap' active' canceling messages store in state' end); check_thread_manager ()) @@ -200,33 +201,36 @@ map_filter (fn (th, (tool', _, _, desc)) => if tool' = tool then SOME (th, (tool', Time.now (), desc)) else NONE) active - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; + val state' = make_state manager timeout_heap [] (killing @ canceling) messages store val _ = if null killing then () else Output.urgent_message ("Interrupted active " ^ das_wort_worker ^ "s.") - in state' end); + in state' end) (* running threads *) fun seconds time = string_of_int (Time.toSeconds time) ^ " s" +fun has_running_threads tool = + exists (fn (_, (tool', _, _, _)) => tool' = tool) + (#active (Synchronized.value global_state)) + fun running_threads tool das_wort_worker = let - val {active, canceling, ...} = Synchronized.value global_state; - - val now = Time.now (); + val {active, canceling, ...} = Synchronized.value global_state + val now = Time.now () fun running_info (_, (tool', birth_time, death_time, desc)) = if tool' = tool then SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ seconds (Time.- (death_time, now)) ^ " to live:\n" ^ - implode_desc desc) + op ^ desc) else NONE fun canceling_info (_, (tool', death_time, desc)) = if tool' = tool then SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^ - seconds (Time.- (now, death_time)) ^ ":\n" ^ implode_desc desc) + seconds (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc) else NONE val running = @@ -241,14 +245,14 @@ fun thread_messages tool das_wort_worker opt_limit = let - val limit = the_default message_display_limit opt_limit; + val limit = the_default message_display_limit opt_limit val tool_store = Synchronized.value global_state |> #store |> filter (curry (op =) tool o fst) val header = "Recent " ^ das_wort_worker ^ " messages" ^ (if length tool_store <= limit then ":" - else " (" ^ string_of_int limit ^ " displayed):"); - val ss = tool_store |> chop limit |> #1 |> map (implode_desc o snd) + else " (" ^ string_of_int limit ^ " displayed):") + val ss = tool_store |> chop limit |> #1 |> map (op ^ o snd) in List.app Output.urgent_message (header :: maps break_into_chunks ss) end end; diff -r 325c8fd0d762 -r 340187063d84 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -15,6 +15,7 @@ type prover_result = Sledgehammer_Provers.prover_result val trace : bool Config.T + val MaShN : string val meshN : string val iterN : string val mashN : string @@ -51,12 +52,15 @@ val mash_suggest_facts : Proof.context -> params -> string -> int -> term list -> term -> fact list -> fact list - val mash_learn_thy : Proof.context -> params -> theory -> Time.time -> unit + val mash_learn_thy : + Proof.context -> params -> theory -> Time.time -> fact list -> string val mash_learn_proof : Proof.context -> params -> term -> thm list -> fact list -> unit val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> fact list -> fact list + val kill_learners : unit -> unit + val running_learners : unit -> unit end; structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = @@ -74,6 +78,8 @@ Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false) fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () +val MaShN = "MaSh" + val meshN = "mesh" val iterN = "iter" val mashN = "mash" @@ -481,8 +487,6 @@ let val thy = Proof_Context.theory_of ctxt val fact_graph = #fact_graph (mash_get ()) -val _ = warning (PolyML.makestring (length (fact_graph |> Graph.keys), length (fact_graph |> Graph.maximals), -length (fact_graph |> Graph.minimals))) (*###*) val parents = parents_wrt_facts facts fact_graph val feats = features_of ctxt prover thy General (concl_t :: hyp_ts) val suggs = @@ -509,34 +513,23 @@ in ((name, parents, feats, deps) :: upds, graph) end val pass1_learn_timeout_factor = 0.5 -val pass2_learn_timeout_factor = 10.0 (* The timeout is understood in a very slack fashion. *) -fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy - timeout = +fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout + facts = let val timer = Timer.startRealTimer () val prover = hd provers fun timed_out frac = Time.> (Timer.checkRealTimer timer, time_mult frac timeout) - val css_table = clasimpset_rule_table_of ctxt - val facts = all_facts_of thy css_table val {fact_graph, ...} = mash_get () fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th) val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd) in if null new_facts then - () + "" else let - val n = length new_facts - val _ = - if verbose then - "MaShing " ^ string_of_int n ^ " fact" ^ plural_s n ^ - " (advisory timeout: " ^ string_from_time timeout ^ ")..." - |> Output.urgent_message - else - () val ths = facts |> map snd val all_names = ths |> filter_out (is_likely_tautology ctxt prover orf is_too_meta) @@ -566,22 +559,15 @@ fact_graph = fact_graph}) end in - TimeLimit.timeLimit (time_mult pass2_learn_timeout_factor timeout) - mash_map trans - handle TimeLimit.TimeOut => - (if verbose then - "MaSh timed out trying to learn " ^ string_of_int n ^ - " fact" ^ plural_s n ^ " in " ^ - string_from_time (Timer.checkRealTimer timer) ^ "." - |> Output.urgent_message - else - ()); - (if verbose then - "MaSh learned " ^ string_of_int n ^ " fact" ^ plural_s n ^ " in " ^ - string_from_time (Timer.checkRealTimer timer) ^ "." - |> Output.urgent_message - else - ()) + mash_map trans; + if verbose then + "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^ + (if verbose then + " in " ^ string_from_time (Timer.checkRealTimer timer) + else + "") ^ "." + else + "" end end @@ -623,19 +609,23 @@ let val thy = Proof_Context.theory_of ctxt fun maybe_learn can_suggest = - if Time.toSeconds timeout >= min_secs_for_learning then - if Multithreading.enabled () then - let - val factor = - if can_suggest then short_learn_timeout_factor - else long_learn_timeout_factor - in - Future.fork (fn () => mash_learn_thy ctxt params thy - (time_mult factor timeout)); () - end - else - mash_learn_thy ctxt params thy - (time_mult short_learn_timeout_factor timeout) + if Async_Manager.has_running_threads MaShN orelse null facts then + () + else if Time.toSeconds timeout >= min_secs_for_learning then + let + val factor = + if can_suggest then short_learn_timeout_factor + else long_learn_timeout_factor + val soft_timeout = time_mult factor timeout + val hard_timeout = time_mult 2.0 soft_timeout + val birth_time = Time.now () + val death_time = Time.+ (birth_time, hard_timeout) + val desc = ("machine learner for Sledgehammer", "") + in + Async_Manager.launch MaShN birth_time death_time desc + (fn () => + (true, mash_learn_thy ctxt params thy soft_timeout facts)) + end else () val fact_filter = @@ -667,4 +657,7 @@ |> not (null add_ths) ? prepend_facts add_ths end +fun kill_learners () = Async_Manager.kill_threads MaShN "learner" +fun running_learners () = Async_Manager.running_threads MaShN "learner" + end; diff -r 325c8fd0d762 -r 340187063d84 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 18 08:44:04 2012 +0200 @@ -33,10 +33,12 @@ val minN = "min" val messagesN = "messages" val supported_proversN = "supported_provers" +val kill_proversN = "kill_provers" val running_proversN = "running_provers" -val kill_proversN = "kill_provers" +val kill_learnersN = "kill_learners" +val running_learnersN = "running_learners" +val unlearnN = "unlearn" val refresh_tptpN = "refresh_tptp" -val reset_mashN = "reset_mash" val auto = Unsynchronized.ref false @@ -374,14 +376,18 @@ messages opt_i else if subcommand = supported_proversN then supported_provers ctxt - else if subcommand = running_proversN then - running_provers () else if subcommand = kill_proversN then kill_provers () + else if subcommand = running_proversN then + running_provers () + else if subcommand = kill_learnersN then + kill_learners () + else if subcommand = running_learnersN then + running_learners () + else if subcommand = unlearnN then + mash_reset ctxt else if subcommand = refresh_tptpN then refresh_systems_on_tptp () - else if subcommand = reset_mashN then - mash_reset ctxt else error ("Unknown subcommand: " ^ quote subcommand ^ ".") end diff -r 325c8fd0d762 -r 340187063d84 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jul 18 08:44:04 2012 +0200 @@ -99,7 +99,7 @@ val smt_slice_fact_frac : real Config.T val smt_slice_time_frac : real Config.T val smt_slice_min_secs : int Config.T - val das_tool : string + val SledgehammerN : string val plain_metis : reconstructor val select_smt_solver : string -> Proof.context -> Proof.context val extract_reconstructor : @@ -153,7 +153,7 @@ (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) -val das_tool = "Sledgehammer" +val SledgehammerN = "Sledgehammer" val reconstructor_names = [metisN, smtN] val plain_metis = Metis (hd partial_type_encs, combsN) @@ -298,9 +298,9 @@ commas (local_provers @ remote_provers) ^ ".") end -fun kill_provers () = Async_Manager.kill_threads das_tool "prover" -fun running_provers () = Async_Manager.running_threads das_tool "prover" -val messages = Async_Manager.thread_messages das_tool "prover" +fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover" +fun running_provers () = Async_Manager.running_threads SledgehammerN "prover" +val messages = Async_Manager.thread_messages SledgehammerN "prover" (** problems, results, ATPs, etc. **) diff -r 325c8fd0d762 -r 340187063d84 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:04 2012 +0200 @@ -53,7 +53,7 @@ fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal = - (name, + (quote name, (if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else @@ -141,7 +141,7 @@ (outcome_code, state) end else - (Async_Manager.launch das_tool birth_time death_time (desc ()) + (Async_Manager.launch SledgehammerN birth_time death_time (desc ()) ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);