# HG changeset patch # User blanchet # Date 1277481936 -7200 # Node ID 9ce2451647d5b7277e3f5f814cc0b1c3c84f2eba # Parent f329e1b99ce6780cdf27259542d76d8ab3f9c1c5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration diff -r f329e1b99ce6 -r 9ce2451647d5 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Jun 25 18:03:01 2010 +0200 +++ b/src/HOL/IsaMakefile Fri Jun 25 18:05:36 2010 +0200 @@ -267,6 +267,7 @@ $(SRC)/Provers/Arith/extract_common_term.ML \ $(SRC)/Tools/cache_io.ML \ $(SRC)/Tools/Metis/metis.ML \ + Tools/ATP_Manager/async_manager.ML \ Tools/ATP_Manager/atp_manager.ML \ Tools/ATP_Manager/atp_systems.ML \ Tools/choice_specification.ML \ diff -r f329e1b99ce6 -r 9ce2451647d5 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Jun 25 18:03:01 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Fri Jun 25 18:05:36 2010 +0200 @@ -19,6 +19,7 @@ ("Tools/Sledgehammer/sledgehammer_fact_filter.ML") ("Tools/Sledgehammer/sledgehammer_tptp_format.ML") ("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") + ("Tools/ATP_Manager/async_manager.ML") ("Tools/ATP_Manager/atp_manager.ML") ("Tools/ATP_Manager/atp_systems.ML") ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML") @@ -97,6 +98,7 @@ use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" use "Tools/Sledgehammer/sledgehammer_tptp_format.ML" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" +use "Tools/ATP_Manager/async_manager.ML" use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_systems.ML" setup ATP_Systems.setup diff -r f329e1b99ce6 -r 9ce2451647d5 src/HOL/Tools/ATP_Manager/async_manager.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP_Manager/async_manager.ML Fri Jun 25 18:05:36 2010 +0200 @@ -0,0 +1,220 @@ +(* Title: HOL/Tools/ATP_Manager/async_manager.ML + Author: Fabian Immler, TU Muenchen + Author: Makarius + Author: Jasmin Blanchette, TU Muenchen + +Central manager for asynchronous diagnosis tool threads. +*) + +signature ASYNC_MANAGER = +sig + val unregister : bool -> string -> Thread.thread -> unit + val register : + string -> bool -> Time.time -> Time.time -> Thread.thread * string -> unit + val kill_threads : string -> unit + val running_threads : string -> unit + val thread_messages : string -> int option -> unit +end; + +structure Async_Manager : ASYNC_MANAGER = +struct + +(** preferences **) + +val message_store_limit = 20; +val message_display_limit = 5; + + +(** thread management **) + +(* data structures over threads *) + +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; + + +(* state of thread manager *) + +type state = + {manager: Thread.thread option, + timeout_heap: Thread_Heap.T, + active: (Thread.thread * (Time.time * Time.time * string)) list, + canceling: (Thread.thread * (Time.time * string)) list, + messages: string list, + store: 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 [] [] [] []); + + +(* unregister thread *) + +fun unregister verbose message thread = + Synchronized.change global_state + (fn state as {manager, timeout_heap, active, canceling, messages, store} => + (case lookup_thread active thread of + SOME (birth_time, _, desc) => + let + val active' = delete_thread thread active; + val now = Time.now () + val canceling' = (thread, (now, desc)) :: canceling + val message' = + desc ^ "\n" ^ message ^ + (if verbose then + "Total time: " ^ Int.toString (Time.toMilliseconds + (Time.- (now, birth_time))) ^ " ms.\n" + else + "") + val messages' = message' :: messages; + val store' = 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)); + + +(* main manager thread -- only one may exist *) + +val min_wait_time = Time.fromMilliseconds 300; +val max_wait_time = Time.fromSeconds 10; + +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 = + map (replace_all "\n\n" "\000") #> maps (space_explode "\000") + +fun print_new_messages tool = + case Synchronized.change_result global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + (messages, make_state manager timeout_heap active canceling [] + store)) of + [] => () + | msgs => + msgs |> break_into_chunks + |> (fn msg :: msgs => tool ^ ": " ^ msg :: msgs) + |> List.app priority + +fun check_thread_manager tool verbose = 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 (Toplevel.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 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 verbose "Timed out.\n"); + print_new_messages tool; + (*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) + + +(* register thread *) + +fun register tool verbose birth_time death_time (thread, desc) = + (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, (birth_time, death_time, desc)) active; + val state' = make_state manager timeout_heap' active' canceling messages store; + in state' end); + check_thread_manager tool verbose); + + + +(** user commands **) + +(* kill threads *) + +fun kill_threads tools = Synchronized.change global_state + (fn {manager, timeout_heap, active, canceling, messages, store} => + let + val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active; + val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; + val _ = if null active then () else priority ("Killed active " ^ tools ^ ".") + in state' end); + + +(* running threads *) + +fun seconds time = string_of_int (Time.toSeconds time) ^ "s"; + +fun running_threads tools = + let + val {active, canceling, ...} = Synchronized.value global_state; + + val now = Time.now (); + fun running_info (_, (birth_time, death_time, desc)) = + "Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ + seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc; + fun canceling_info (_, (deadth_time, desc)) = + "Trying to interrupt thread since " ^ seconds (Time.- (now, deadth_time)) ^ ":\n" ^ desc; + + val running = + case map running_info active of + [] => ["No " ^ tools ^ " running."] + | ss => "Running " ^ tools ^ ":" :: ss + val interrupting = + case map canceling_info canceling of + [] => [] + | ss => "Trying to interrupt the following " ^ tools ^ ":" :: ss + in priority (space_implode "\n\n" (running @ interrupting)) end + +fun thread_messages tool opt_limit = + let + val limit = the_default message_display_limit opt_limit; + val {store, ...} = Synchronized.value global_state; + val header = + "Recent " ^ tool ^ " messages" ^ + (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):"); + in List.app priority (header :: break_into_chunks (#1 (chop limit store))) end + +end; diff -r f329e1b99ce6 -r 9ce2451647d5 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Jun 25 18:03:01 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Jun 25 18:05:36 2010 +0200 @@ -67,6 +67,13 @@ open Metis_Clauses open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct +open Async_Manager + +(** The Sledgehammer **) + +fun kill_atps () = kill_threads "ATPs" +fun running_atps () = running_threads "ATPs" +val messages = thread_messages "ATP" (** problems, results, provers, etc. **) @@ -112,210 +119,6 @@ type prover = params -> minimize_command -> Time.time -> problem -> prover_result - -(** preferences **) - -val message_store_limit = 20; -val message_display_limit = 5; - - -(** thread management **) - -(* data structures over threads *) - -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; - - -(* state of thread manager *) - -type state = - {manager: Thread.thread option, - timeout_heap: Thread_Heap.T, - active: (Thread.thread * (Time.time * Time.time * string)) list, - canceling: (Thread.thread * (Time.time * string)) list, - messages: string list, - store: 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 "atp_manager" - (make_state NONE Thread_Heap.empty [] [] [] []); - - -(* unregister ATP thread *) - -fun unregister verbose message thread = - Synchronized.change global_state - (fn state as {manager, timeout_heap, active, canceling, messages, store} => - (case lookup_thread active thread of - SOME (birth_time, _, desc) => - let - val active' = delete_thread thread active; - val now = Time.now () - val canceling' = (thread, (now, desc)) :: canceling - val message' = - desc ^ "\n" ^ message ^ - (if verbose then - "Total time: " ^ Int.toString (Time.toMilliseconds - (Time.- (now, birth_time))) ^ " ms.\n" - else - "") - val messages' = message' :: messages; - val store' = 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)); - - -(* main manager thread -- only one may exist *) - -val min_wait_time = Time.fromMilliseconds 300; -val max_wait_time = Time.fromSeconds 10; - -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 = - map (replace_all "\n\n" "\000") #> maps (space_explode "\000") - -fun print_new_messages () = - case Synchronized.change_result global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - (messages, make_state manager timeout_heap active canceling [] - store)) of - [] => () - | msgs => - msgs |> break_into_chunks - |> (fn msg :: msgs => "Sledgehammer: " ^ msg :: msgs) - |> List.app priority - -fun check_thread_manager verbose = 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 (Toplevel.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 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 verbose "Timed out.\n"); - 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) - - -(* register ATP thread *) - -fun register verbose birth_time death_time (thread, desc) = - (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, (birth_time, death_time, desc)) active; - val state' = make_state manager timeout_heap' active' canceling messages store; - in state' end); - check_thread_manager verbose); - - - -(** user commands **) - -(* kill ATPs *) - -fun kill_atps () = Synchronized.change global_state - (fn {manager, timeout_heap, active, canceling, messages, store} => - let - val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active; - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store; - val _ = if null active then () - else priority "Killed active Sledgehammer threads." - in state' end); - - -(* running_atps *) - -fun seconds time = string_of_int (Time.toSeconds time) ^ "s"; - -fun running_atps () = - let - val {active, canceling, ...} = Synchronized.value global_state; - - val now = Time.now (); - fun running_info (_, (birth_time, death_time, desc)) = - "Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^ - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc; - fun canceling_info (_, (deadth_time, desc)) = - "Trying to interrupt thread since " ^ seconds (Time.- (now, deadth_time)) ^ ":\n" ^ desc; - - val running = - if null active then "No ATPs running." - else space_implode "\n\n" ("Running ATPs:" :: map running_info active); - val interrupting = - if null canceling then - "" - else - space_implode "\n\n" ("Trying to interrupt the following ATPs:" :: - map canceling_info canceling) - in priority (running ^ "\n" ^ interrupting) end; - -fun messages opt_limit = - let - val limit = the_default message_display_limit opt_limit; - val {store, ...} = Synchronized.value global_state; - val header = - "Recent ATP messages" ^ - (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):"); - in List.app priority (header :: break_into_chunks (#1 (chop limit store))) end - - -(** The Sledgehammer **) - (* named provers *) structure Data = Theory_Data @@ -353,7 +156,8 @@ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); val _ = Toplevel.thread true (fn () => let - val _ = register verbose birth_time death_time (Thread.self (), desc) + val _ = register "Sledgehammer" verbose birth_time death_time + (Thread.self (), desc) val problem = {subgoal = i, goal = (ctxt, (facts, goal)), relevance_override = relevance_override, axiom_clauses = NONE,