# HG changeset patch # User blanchet # Date 1443813325 -7200 # Node ID 6d779a71086d8fd1128259673561104e60a96fce # Parent 150aa3015c478d6435db1e8317619ed71fe696ca further reduced dependency on legacy async thread manager diff -r 150aa3015c47 -r 6d779a71086d src/HOL/Tools/Sledgehammer/async_manager_legacy.ML --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Fri Oct 02 21:15:25 2015 +0200 @@ -10,13 +10,9 @@ signature ASYNC_MANAGER_LEGACY = sig - val break_into_chunks : string -> string list val thread : 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; structure Async_Manager_Legacy : ASYNC_MANAGER_LEGACY = @@ -31,9 +27,6 @@ Simple_Thread.attributes {name = "async_manager", stack_limit = NONE, interrupts = interrupts}); -val message_store_limit = 20 -val message_display_limit = 10 - fun implode_message (workers, work) = space_implode " " (Try.serial_commas "and" workers) ^ work @@ -54,18 +47,17 @@ (Thread.thread * (string * Time.time * Time.time * (string * string))) list, canceling: (Thread.thread * (string * Time.time * (string * string))) list, - messages: (bool * (string * (string * string))) list, - store: (string * (string * string)) list} + messages: (bool * (string * (string * string))) list} -fun make_state manager timeout_heap active canceling messages store : state = - {manager = manager, timeout_heap = timeout_heap, active = active, - canceling = canceling, messages = messages, store = store} +fun make_state manager timeout_heap active canceling messages : state = + {manager = manager, timeout_heap = timeout_heap, active = active, canceling = canceling, + messages = messages} -val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] [] []) +val global_state = Synchronized.var "async_manager" (make_state NONE Thread_Heap.empty [] [] []) fun unregister (urgent, message) thread = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => + (fn state as {manager, timeout_heap, active, canceling, messages} => (case lookup_thread active thread of SOME (tool, _, _, desc as (worker, its_desc)) => let @@ -75,50 +67,30 @@ 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)) - in make_state manager timeout_heap active' canceling' messages' store' end + in make_state manager timeout_heap active' canceling' messages' end | NONE => state)) val min_wait_time = seconds 0.3 val max_wait_time = seconds 10.0 -fun replace_all bef aft = - let - fun aux seen "" = String.implode (rev seen) - | aux seen s = - if String.isPrefix bef s then - aux seen "" ^ aft ^ aux [] (unprefix bef s) - else - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE)) - in aux [] end - -(* This is a workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in - "proof" is not highlighted. *) -val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000" - fun print_new_messages () = Synchronized.change_result global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => + (fn {manager, timeout_heap, active, canceling, messages} => messages |> List.partition (fn (urgent, _) => (null active andalso null canceling) orelse urgent) - ||> (fn postponed_messages => - make_state manager timeout_heap active canceling - postponed_messages store)) + ||> make_state manager timeout_heap active canceling) |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker)) |> AList.group (op =) |> List.app (fn ((_, ""), _) => () | ((tool, work), workers) => tool ^ ": " ^ implode_message (workers |> sort_distinct string_ord, work) - |> break_into_chunks - |> List.app writeln) + |> writeln) fun check_thread_manager () = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => + (fn state as {manager, timeout_heap, active, canceling, messages} => if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state else let val manager = SOME (make_thread false (fn () => let @@ -128,7 +100,7 @@ | SOME (time, _) => time) (*action: find threads whose timeout is reached, and interrupt canceling threads*) - fun action {manager, timeout_heap, active, canceling, messages, store} = + fun action {manager, timeout_heap, active, canceling, messages} = let val (timeout_threads, timeout_heap') = Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap in @@ -138,14 +110,14 @@ 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 in SOME (map #2 timeout_threads, state') end end in while Synchronized.change_result global_state - (fn state as {timeout_heap, active, canceling, messages, store, ...} => + (fn state as {timeout_heap, active, canceling, messages, ...} => if null active andalso null canceling andalso null messages - then (false, make_state NONE timeout_heap active canceling messages store) + then (false, make_state NONE timeout_heap active canceling messages) else (true, state)) do (Synchronized.timed_access global_state @@ -156,15 +128,15 @@ (* 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) + in make_state manager timeout_heap active canceling messages end) fun register tool birth_time death_time desc thread = (Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => + (fn {manager, timeout_heap, active, canceling, messages} => 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 state' = make_state manager timeout_heap' active' canceling messages in state' end); check_thread_manager ()) @@ -177,60 +149,7 @@ in unregister (f ()) self end); ()) -fun kill_threads tool das_wort_worker = Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val killing = - 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 _ = - if null killing then () - else writeln ("Interrupted active " ^ das_wort_worker ^ "s.") - in state' end) - -fun str_of_time 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 () - fun running_info (_, (tool', birth_time, death_time, desc)) = - if tool' = tool then - SOME ("Running: " ^ str_of_time (Time.- (now, birth_time)) ^ " -- " ^ - str_of_time (Time.- (death_time, now)) ^ " to live:\n" ^ op ^ desc) - else - NONE - fun canceling_info (_, (tool', death_time, desc)) = - if tool' = tool then - SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^ - str_of_time (Time.- (now, death_time)) ^ ":\n" ^ op ^ desc) - else - NONE - val running = - case map_filter running_info active of - [] => ["No " ^ das_wort_worker ^ "s running."] - | ss => "Running " ^ das_wort_worker ^ "s" :: ss - val interrupting = - case map_filter canceling_info canceling of - [] => [] - | ss => "Interrupting " ^ das_wort_worker ^ "s" :: ss - in writeln (space_implode "\n\n" (running @ interrupting)) end - -fun thread_messages tool das_wort_worker opt_limit = - let - 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 (op ^ o snd) - in List.app writeln (header :: maps break_into_chunks ss) end - end; diff -r 150aa3015c47 -r 6d779a71086d src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 02 21:15:25 2015 +0200 @@ -60,10 +60,6 @@ ordered_outcome_codes |> the_default unknownN -fun prover_description verbose name num_facts = - (quote name, - if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "") - fun is_metis_method (Metis_Method _) = true | is_metis_method _ = false @@ -125,8 +121,6 @@ val hard_timeout = time_mult 3.0 timeout val _ = spying spy (fn () => (state, subgoal, name, "Launched")); - val birth_time = Time.now () - val death_time = Time.+ (birth_time, hard_timeout) 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 @@ -228,12 +222,8 @@ 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 - outcome - |> Async_Manager_Legacy.break_into_chunks - |> List.app writeln + if outcome <> "" andalso is_some writeln_result then the writeln_result outcome + else writeln outcome in (outcome_code, []) end end diff -r 150aa3015c47 -r 6d779a71086d src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 02 21:15:25 2015 +0200 @@ -33,8 +33,6 @@ val runN = "run" val supported_proversN = "supported_provers" -val kill_learnersN = "kill_learners" -val running_learnersN = "running_learners" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) @@ -326,8 +324,6 @@ end else if subcommand = supported_proversN then supported_provers ctxt - else if subcommand = kill_learnersN then - kill_learners () else if subcommand = unlearnN then mash_unlearn () else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse @@ -343,8 +339,6 @@ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) - else if subcommand = running_learnersN then - running_learners () else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else diff -r 150aa3015c47 -r 6d779a71086d src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Oct 02 21:15:25 2015 +0200 @@ -76,7 +76,7 @@ fun postprocess_isar_proof_remove_show_stuttering (Proof (fix, assms, steps)) = let fun process_steps [] = [] - | process_steps (steps as [Prove ([], [], l1, t1, subs1, facts1, meths1, comment1), + | process_steps (steps as [Prove ([], [], _, t1, subs1, facts1, meths1, comment1), Prove ([Show], [], l2, t2, _, _, _, comment2)]) = if t1 aconv t2 then [Prove ([Show], [], l2, t2, subs1, facts1, meths1, comment1 ^ comment2)] else steps diff -r 150aa3015c47 -r 6d779a71086d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 02 21:06:32 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Oct 02 21:15:25 2015 +0200 @@ -81,8 +81,6 @@ val mash_weight : real val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> raw_fact list -> (string * fact list) list - val kill_learners : unit -> unit - val running_learners : unit -> unit end; structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH = @@ -1600,7 +1598,4 @@ | _ => [(effective_fact_filter, mesh)]) end -fun kill_learners () = Async_Manager_Legacy.kill_threads MaShN "learner" -fun running_learners () = Async_Manager_Legacy.running_threads MaShN "learner" - end;