factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
--- 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 \
--- 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
--- /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;
--- 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,