--- 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 \<noteq> size y \<Longrightarrow> x \<noteq> 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"
--- 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;
--- /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;
--- 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, []))
--- 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;
--- 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;