# HG changeset patch # User wenzelm # Date 1422545729 -3600 # Node ID ca459352d8c5365973baefa317417c8f9cf6b2d4 # Parent 31d810570879c18a9f88aefe43c9a06214354cc4 more explicit indication of Async_Manager_Legacy as Proof General legacy; diff -r 31d810570879 -r ca459352d8c5 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Jan 29 16:16:01 2015 +0100 +++ b/src/HOL/Sledgehammer.thy Thu Jan 29 16:35:29 2015 +0100 @@ -14,7 +14,7 @@ lemma size_ne_size_imp_ne: "size x \ size y \ x \ y" by (erule contrapos_nn) (rule arg_cong) -ML_file "Tools/Sledgehammer/async_manager.ML" +ML_file "Tools/Sledgehammer/async_manager_legacy.ML" ML_file "Tools/Sledgehammer/sledgehammer_util.ML" ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML" diff -r 31d810570879 -r ca459352d8c5 src/HOL/Tools/Sledgehammer/async_manager.ML --- a/src/HOL/Tools/Sledgehammer/async_manager.ML Thu Jan 29 16:16:01 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,235 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/async_manager.ML - Author: Fabian Immler, TU Muenchen - Author: Makarius - Author: Jasmin Blanchette, TU Muenchen - -Central manager for asynchronous diagnosis tool threads. - -Proof General legacy! -*) - -signature ASYNC_MANAGER = -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 : ASYNC_MANAGER = -struct - -fun make_thread interrupts body = - Thread.fork - (fn () => - Runtime.debugging NONE body () handle exn => - if Exn.is_interrupt exn then () - else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn), - Simple_Thread.attributes {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 - -structure Thread_Heap = Heap -( - 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 - -type state = - {manager: Thread.thread option, - timeout_heap: Thread_Heap.T, - active: - (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} - -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} - -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} => - (case lookup_thread active thread of - SOME (tool, _, _, desc as (worker, its_desc)) => - let - val active' = delete_thread thread active - val now = Time.now () - val canceling' = (thread, (tool, now, desc)) :: canceling - 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 - | 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} => - 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)) - |> 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) - -fun check_thread_manager () = Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state - else let val manager = SOME (make_thread false (fn () => - let - fun time_limit timeout_heap = - (case try Thread_Heap.min timeout_heap of - NONE => Time.+ (Time.now (), max_wait_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 - in - if null timeout_threads andalso null canceling then - NONE - else - 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 - 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, ...} => - if null active andalso null canceling andalso null messages - 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) - end)) - in make_state manager timeout_heap active canceling messages store end) - -fun register tool birth_time death_time desc thread = - (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 - in state' end); - check_thread_manager ()) - -fun thread tool birth_time death_time desc f = - (make_thread true - (fn () => - let - val self = Thread.self () - val _ = register tool birth_time death_time desc self - 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 31d810570879 -r ca459352d8c5 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Thu Jan 29 16:35:29 2015 +0100 @@ -0,0 +1,235 @@ +(* Title: HOL/Tools/Sledgehammer/async_manager_legacy.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Central manager for asynchronous diagnosis tool threads. + +Proof General legacy! +*) + +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 = +struct + +fun make_thread interrupts body = + Thread.fork + (fn () => + Runtime.debugging NONE body () handle exn => + if Exn.is_interrupt exn then () + else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn), + Simple_Thread.attributes {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 + +structure Thread_Heap = Heap +( + 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 + +type state = + {manager: Thread.thread option, + timeout_heap: Thread_Heap.T, + active: + (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} + +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} + +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} => + (case lookup_thread active thread of + SOME (tool, _, _, desc as (worker, its_desc)) => + let + val active' = delete_thread thread active + val now = Time.now () + val canceling' = (thread, (tool, now, desc)) :: canceling + 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 + | 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} => + 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)) + |> 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) + +fun check_thread_manager () = Synchronized.change global_state + (fn state as {manager, timeout_heap, active, canceling, messages, store} => + if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state + else let val manager = SOME (make_thread false (fn () => + let + fun time_limit timeout_heap = + (case try Thread_Heap.min timeout_heap of + NONE => Time.+ (Time.now (), max_wait_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 + in + if null timeout_threads andalso null canceling then + NONE + else + 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 + 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, ...} => + if null active andalso null canceling andalso null messages + 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) + end)) + in make_state manager timeout_heap active canceling messages store end) + +fun register tool birth_time death_time desc thread = + (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 + in state' end); + check_thread_manager ()) + +fun thread tool birth_time death_time desc f = + (make_thread true + (fn () => + let + val self = Thread.self () + val _ = register tool birth_time death_time desc self + 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 31d810570879 -r ca459352d8c5 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jan 29 16:16:01 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jan 29 16:35:29 2015 +0100 @@ -225,11 +225,11 @@ the output_result outcome else outcome - |> Async_Manager.break_into_chunks + |> Async_Manager_Legacy.break_into_chunks |> List.app writeln in (outcome_code, []) end else - (Async_Manager.thread SledgehammerN birth_time death_time + (Async_Manager_Legacy.thread SledgehammerN birth_time death_time (prover_description verbose name num_facts) ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go); (unknownN, [])) diff -r 31d810570879 -r ca459352d8c5 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 29 16:16:01 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 29 16:35:29 2015 +0100 @@ -1256,7 +1256,7 @@ val death_time = Time.+ (birth_time, hard_timeout) val desc = ("Machine learner for Sledgehammer", "") in - Async_Manager.thread MaShN birth_time death_time desc task + Async_Manager_Legacy.thread MaShN birth_time death_time desc task end fun learned_proof_name () = @@ -1519,7 +1519,7 @@ val thy = Proof_Context.theory_of ctxt fun maybe_launch_thread exact min_num_facts_to_learn = - if not (Async_Manager.has_running_threads MaShN) andalso + if not (Async_Manager_Legacy.has_running_threads MaShN) andalso Time.toSeconds timeout >= min_secs_for_learning then let val timeout = time_mult learn_timeout_slack timeout in (if verbose then @@ -1598,7 +1598,7 @@ | _ => [(effective_fact_filter, mesh)]) end -fun kill_learners () = Async_Manager.kill_threads MaShN "learner" -fun running_learners () = Async_Manager.running_threads MaShN "learner" +fun kill_learners () = Async_Manager_Legacy.kill_threads MaShN "learner" +fun running_learners () = Async_Manager_Legacy.running_threads MaShN "learner" end; diff -r 31d810570879 -r ca459352d8c5 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Jan 29 16:16:01 2015 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Jan 29 16:35:29 2015 +0100 @@ -201,8 +201,8 @@ writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") end -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" +fun kill_provers () = Async_Manager_Legacy.kill_threads SledgehammerN "prover" +fun running_provers () = Async_Manager_Legacy.running_threads SledgehammerN "prover" +val messages = Async_Manager_Legacy.thread_messages SledgehammerN "prover" end;