1.1 --- a/src/HOL/HOL.thy Tue Dec 07 10:03:43 2010 +0100
1.2 +++ b/src/HOL/HOL.thy Tue Dec 07 11:50:16 2010 +0100
1.3 @@ -29,8 +29,6 @@
1.4 "~~/src/Tools/induct.ML"
1.5 ("~~/src/Tools/induct_tacs.ML")
1.6 ("Tools/recfun_codegen.ML")
1.7 - "Tools/async_manager.ML"
1.8 - "Tools/try.ML"
1.9 ("Tools/cnf_funcs.ML")
1.10 "~~/src/Tools/subtyping.ML"
1.11 begin
1.12 @@ -1982,10 +1980,6 @@
1.13 *} "solve goal by normalization"
1.14
1.15
1.16 -subsection {* Try *}
1.17 -
1.18 -setup {* Try.setup *}
1.19 -
1.20 subsection {* Counterexample Search Units *}
1.21
1.22 subsubsection {* Quickcheck *}
2.1 --- a/src/HOL/IsaMakefile Tue Dec 07 10:03:43 2010 +0100
2.2 +++ b/src/HOL/IsaMakefile Tue Dec 07 11:50:16 2010 +0100
2.3 @@ -224,7 +224,6 @@
2.4 Tools/Metis/metis_translate.ML \
2.5 Tools/abel_cancel.ML \
2.6 Tools/arith_data.ML \
2.7 - Tools/async_manager.ML \
2.8 Tools/cnf_funcs.ML \
2.9 Tools/dseq.ML \
2.10 Tools/inductive.ML \
2.11 @@ -344,6 +343,7 @@
2.12 Tools/recdef.ML \
2.13 Tools/record.ML \
2.14 Tools/semiring_normalizer.ML \
2.15 + Tools/Sledgehammer/async_manager.ML \
2.16 Tools/Sledgehammer/sledgehammer.ML \
2.17 Tools/Sledgehammer/sledgehammer_filter.ML \
2.18 Tools/Sledgehammer/sledgehammer_minimize.ML \
3.1 --- a/src/HOL/Metis.thy Tue Dec 07 10:03:43 2010 +0100
3.2 +++ b/src/HOL/Metis.thy Tue Dec 07 11:50:16 2010 +0100
3.3 @@ -12,6 +12,7 @@
3.4 ("Tools/Metis/metis_translate.ML")
3.5 ("Tools/Metis/metis_reconstruct.ML")
3.6 ("Tools/Metis/metis_tactics.ML")
3.7 + ("Tools/try.ML")
3.8 begin
3.9
3.10 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
3.11 @@ -38,4 +39,10 @@
3.12 hide_const (open) fequal
3.13 hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
3.14
3.15 +subsection {* Try *}
3.16 +
3.17 +use "Tools/try.ML"
3.18 +
3.19 +setup {* Try.setup *}
3.20 +
3.21 end
4.1 --- a/src/HOL/Sledgehammer.thy Tue Dec 07 10:03:43 2010 +0100
4.2 +++ b/src/HOL/Sledgehammer.thy Tue Dec 07 11:50:16 2010 +0100
4.3 @@ -8,7 +8,8 @@
4.4
4.5 theory Sledgehammer
4.6 imports ATP SMT
4.7 -uses "Tools/Sledgehammer/sledgehammer_util.ML"
4.8 +uses "Tools/Sledgehammer/async_manager.ML"
4.9 + "Tools/Sledgehammer/sledgehammer_util.ML"
4.10 "Tools/Sledgehammer/sledgehammer_filter.ML"
4.11 "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
4.12 "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Dec 07 10:03:43 2010 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Dec 07 11:50:16 2010 +0100
5.3 @@ -133,8 +133,9 @@
5.4 Type (s, _) =>
5.5 let val s' = shortest_name s in
5.6 prefix ^
5.7 - (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
5.8 - atom_suffix s m
5.9 + (if T = @{typ string} then "s"
5.10 + else if String.isPrefix "\\" s' then s'
5.11 + else substring (s', 0, 1)) ^ atom_suffix s m
5.12 end
5.13 | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
5.14 | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
6.1 --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 10:03:43 2010 +0100
6.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 11:50:16 2010 +0100
6.3 @@ -216,7 +216,22 @@
6.4 else ()
6.5 end
6.6
6.7 -fun gen_solver name info rm ctxt irules =
6.8 +
6.9 +
6.10 +(* registry *)
6.11 +
6.12 +type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
6.13 +
6.14 +type solver_info = {
6.15 + env_var: string,
6.16 + is_remote: bool,
6.17 + options: Proof.context -> string list,
6.18 + interface: interface,
6.19 + reconstruct: string list * SMT_Translate.recon -> Proof.context ->
6.20 + (int list * thm) * Proof.context,
6.21 + default_max_relevant: int }
6.22 +
6.23 +fun gen_solver name (info : solver_info) rm ctxt irules =
6.24 let
6.25 val {env_var, is_remote, options, interface, reconstruct, ...} = info
6.26 val {extra_norm, translate} = interface
6.27 @@ -235,21 +250,6 @@
6.28 |> pair idxs)
6.29 end
6.30
6.31 -
6.32 -
6.33 -(* registry *)
6.34 -
6.35 -type solver = bool option -> Proof.context -> (int * thm) list -> int list * thm
6.36 -
6.37 -type solver_info = {
6.38 - env_var: string,
6.39 - is_remote: bool,
6.40 - options: Proof.context -> string list,
6.41 - interface: interface,
6.42 - reconstruct: string list * SMT_Translate.recon -> Proof.context ->
6.43 - (int list * thm) * Proof.context,
6.44 - default_max_relevant: int }
6.45 -
6.46 structure Solvers = Generic_Data
6.47 (
6.48 type T = solver_info Symtab.table
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Tue Dec 07 11:50:16 2010 +0100
7.3 @@ -0,0 +1,237 @@
7.4 +(* Title: HOL/Tools/Sledgehammer/async_manager.ML
7.5 + Author: Fabian Immler, TU Muenchen
7.6 + Author: Makarius
7.7 + Author: Jasmin Blanchette, TU Muenchen
7.8 +
7.9 +Central manager for asynchronous diagnosis tool threads.
7.10 +*)
7.11 +
7.12 +signature ASYNC_MANAGER =
7.13 +sig
7.14 + val break_into_chunks : string list -> string list
7.15 + val launch :
7.16 + string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
7.17 + val kill_threads : string -> string -> unit
7.18 + val running_threads : string -> string -> unit
7.19 + val thread_messages : string -> string -> int option -> unit
7.20 +end;
7.21 +
7.22 +structure Async_Manager : ASYNC_MANAGER =
7.23 +struct
7.24 +
7.25 +(** preferences **)
7.26 +
7.27 +val message_store_limit = 20;
7.28 +val message_display_limit = 5;
7.29 +
7.30 +
7.31 +(** thread management **)
7.32 +
7.33 +(* data structures over threads *)
7.34 +
7.35 +structure Thread_Heap = Heap
7.36 +(
7.37 + type elem = Time.time * Thread.thread;
7.38 + fun ord ((a, _), (b, _)) = Time.compare (a, b);
7.39 +);
7.40 +
7.41 +fun lookup_thread xs = AList.lookup Thread.equal xs;
7.42 +fun delete_thread xs = AList.delete Thread.equal xs;
7.43 +fun update_thread xs = AList.update Thread.equal xs;
7.44 +
7.45 +
7.46 +(* state of thread manager *)
7.47 +
7.48 +type state =
7.49 + {manager: Thread.thread option,
7.50 + timeout_heap: Thread_Heap.T,
7.51 + active: (Thread.thread * (string * Time.time * Time.time * string)) list,
7.52 + canceling: (Thread.thread * (string * Time.time * string)) list,
7.53 + messages: (string * string) list,
7.54 + store: (string * string) list}
7.55 +
7.56 +fun make_state manager timeout_heap active canceling messages store : state =
7.57 + {manager = manager, timeout_heap = timeout_heap, active = active,
7.58 + canceling = canceling, messages = messages, store = store}
7.59 +
7.60 +val global_state = Synchronized.var "async_manager"
7.61 + (make_state NONE Thread_Heap.empty [] [] [] []);
7.62 +
7.63 +
7.64 +(* unregister thread *)
7.65 +
7.66 +fun unregister message thread =
7.67 + Synchronized.change global_state
7.68 + (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
7.69 + (case lookup_thread active thread of
7.70 + SOME (tool, _, _, desc) =>
7.71 + let
7.72 + val active' = delete_thread thread active;
7.73 + val now = Time.now ()
7.74 + val canceling' = (thread, (tool, now, desc)) :: canceling
7.75 + val message' = desc ^ "\n" ^ message
7.76 + val messages' = (tool, message') :: messages;
7.77 + val store' = (tool, message') ::
7.78 + (if length store <= message_store_limit then store
7.79 + else #1 (chop message_store_limit store));
7.80 + in make_state manager timeout_heap active' canceling' messages' store' end
7.81 + | NONE => state));
7.82 +
7.83 +
7.84 +(* main manager thread -- only one may exist *)
7.85 +
7.86 +val min_wait_time = seconds 0.3;
7.87 +val max_wait_time = seconds 10.0;
7.88 +
7.89 +fun replace_all bef aft =
7.90 + let
7.91 + fun aux seen "" = String.implode (rev seen)
7.92 + | aux seen s =
7.93 + if String.isPrefix bef s then
7.94 + aux seen "" ^ aft ^ aux [] (unprefix bef s)
7.95 + else
7.96 + aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
7.97 + in aux [] end
7.98 +
7.99 +(* This is a workaround for Proof General's off-by-a-few sendback display bug,
7.100 + whereby "pr" in "proof" is not highlighted. *)
7.101 +val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
7.102 +
7.103 +fun print_new_messages () =
7.104 + case Synchronized.change_result global_state
7.105 + (fn {manager, timeout_heap, active, canceling, messages, store} =>
7.106 + (messages, make_state manager timeout_heap active canceling []
7.107 + store)) of
7.108 + [] => ()
7.109 + | msgs as (tool, _) :: _ =>
7.110 + let val ss = break_into_chunks (map snd msgs) in
7.111 + List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
7.112 + end
7.113 +
7.114 +fun check_thread_manager () = Synchronized.change global_state
7.115 + (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
7.116 + if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
7.117 + else let val manager = SOME (Toplevel.thread false (fn () =>
7.118 + let
7.119 + fun time_limit timeout_heap =
7.120 + (case try Thread_Heap.min timeout_heap of
7.121 + NONE => Time.+ (Time.now (), max_wait_time)
7.122 + | SOME (time, _) => time);
7.123 +
7.124 + (*action: find threads whose timeout is reached, and interrupt canceling threads*)
7.125 + fun action {manager, timeout_heap, active, canceling, messages, store} =
7.126 + let val (timeout_threads, timeout_heap') =
7.127 + Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
7.128 + in
7.129 + if null timeout_threads andalso null canceling then
7.130 + NONE
7.131 + else
7.132 + let
7.133 + val _ = List.app (Simple_Thread.interrupt o #1) canceling
7.134 + val canceling' = filter (Thread.isActive o #1) canceling
7.135 + val state' = make_state manager timeout_heap' active canceling' messages store;
7.136 + in SOME (map #2 timeout_threads, state') end
7.137 + end;
7.138 + in
7.139 + while Synchronized.change_result global_state
7.140 + (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
7.141 + if null active andalso null canceling andalso null messages
7.142 + then (false, make_state NONE timeout_heap active canceling messages store)
7.143 + else (true, state))
7.144 + do
7.145 + (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
7.146 + |> these
7.147 + |> List.app (unregister "Timed out.\n");
7.148 + print_new_messages ();
7.149 + (*give threads some time to respond to interrupt*)
7.150 + OS.Process.sleep min_wait_time)
7.151 + end))
7.152 + in make_state manager timeout_heap active canceling messages store end)
7.153 +
7.154 +
7.155 +(* register thread *)
7.156 +
7.157 +fun register tool birth_time death_time desc thread =
7.158 + (Synchronized.change global_state
7.159 + (fn {manager, timeout_heap, active, canceling, messages, store} =>
7.160 + let
7.161 + val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
7.162 + val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
7.163 + val state' = make_state manager timeout_heap' active' canceling messages store;
7.164 + in state' end);
7.165 + check_thread_manager ())
7.166 +
7.167 +
7.168 +fun launch tool birth_time death_time desc f =
7.169 + (Toplevel.thread true
7.170 + (fn () =>
7.171 + let
7.172 + val self = Thread.self ()
7.173 + val _ = register tool birth_time death_time desc self
7.174 + val message = f ()
7.175 + in unregister message self end);
7.176 + ())
7.177 +
7.178 +
7.179 +(** user commands **)
7.180 +
7.181 +(* kill threads *)
7.182 +
7.183 +fun kill_threads tool workers = Synchronized.change global_state
7.184 + (fn {manager, timeout_heap, active, canceling, messages, store} =>
7.185 + let
7.186 + val killing =
7.187 + map_filter (fn (th, (tool', _, _, desc)) =>
7.188 + if tool' = tool then SOME (th, (tool', Time.now (), desc))
7.189 + else NONE) active
7.190 + val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
7.191 + val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
7.192 + in state' end);
7.193 +
7.194 +
7.195 +(* running threads *)
7.196 +
7.197 +fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
7.198 +
7.199 +fun running_threads tool workers =
7.200 + let
7.201 + val {active, canceling, ...} = Synchronized.value global_state;
7.202 +
7.203 + val now = Time.now ();
7.204 + fun running_info (_, (tool', birth_time, death_time, desc)) =
7.205 + if tool' = tool then
7.206 + SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
7.207 + seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
7.208 + else
7.209 + NONE
7.210 + fun canceling_info (_, (tool', death_time, desc)) =
7.211 + if tool' = tool then
7.212 + SOME ("Trying to interrupt thread since " ^
7.213 + seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
7.214 + else
7.215 + NONE
7.216 + val running =
7.217 + case map_filter running_info active of
7.218 + [] => ["No " ^ workers ^ " running."]
7.219 + | ss => "Running " ^ workers ^ ":" :: ss
7.220 + val interrupting =
7.221 + case map_filter canceling_info canceling of
7.222 + [] => []
7.223 + | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
7.224 + in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
7.225 +
7.226 +fun thread_messages tool worker opt_limit =
7.227 + let
7.228 + val limit = the_default message_display_limit opt_limit;
7.229 + val tool_store = Synchronized.value global_state
7.230 + |> #store |> filter (curry (op =) tool o fst)
7.231 + val header =
7.232 + "Recent " ^ worker ^ " messages" ^
7.233 + (if length tool_store <= limit then ":"
7.234 + else " (" ^ string_of_int limit ^ " displayed):");
7.235 + in
7.236 + List.app Output.urgent_message (header :: break_into_chunks
7.237 + (map snd (#1 (chop limit tool_store))))
7.238 + end
7.239 +
7.240 +end;
8.1 --- a/src/HOL/Tools/async_manager.ML Tue Dec 07 10:03:43 2010 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,237 +0,0 @@
8.4 -(* Title: HOL/Tools/async_manager.ML
8.5 - Author: Fabian Immler, TU Muenchen
8.6 - Author: Makarius
8.7 - Author: Jasmin Blanchette, TU Muenchen
8.8 -
8.9 -Central manager for asynchronous diagnosis tool threads.
8.10 -*)
8.11 -
8.12 -signature ASYNC_MANAGER =
8.13 -sig
8.14 - val break_into_chunks : string list -> string list
8.15 - val launch :
8.16 - string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
8.17 - val kill_threads : string -> string -> unit
8.18 - val running_threads : string -> string -> unit
8.19 - val thread_messages : string -> string -> int option -> unit
8.20 -end;
8.21 -
8.22 -structure Async_Manager : ASYNC_MANAGER =
8.23 -struct
8.24 -
8.25 -(** preferences **)
8.26 -
8.27 -val message_store_limit = 20;
8.28 -val message_display_limit = 5;
8.29 -
8.30 -
8.31 -(** thread management **)
8.32 -
8.33 -(* data structures over threads *)
8.34 -
8.35 -structure Thread_Heap = Heap
8.36 -(
8.37 - type elem = Time.time * Thread.thread;
8.38 - fun ord ((a, _), (b, _)) = Time.compare (a, b);
8.39 -);
8.40 -
8.41 -fun lookup_thread xs = AList.lookup Thread.equal xs;
8.42 -fun delete_thread xs = AList.delete Thread.equal xs;
8.43 -fun update_thread xs = AList.update Thread.equal xs;
8.44 -
8.45 -
8.46 -(* state of thread manager *)
8.47 -
8.48 -type state =
8.49 - {manager: Thread.thread option,
8.50 - timeout_heap: Thread_Heap.T,
8.51 - active: (Thread.thread * (string * Time.time * Time.time * string)) list,
8.52 - canceling: (Thread.thread * (string * Time.time * string)) list,
8.53 - messages: (string * string) list,
8.54 - store: (string * string) list}
8.55 -
8.56 -fun make_state manager timeout_heap active canceling messages store : state =
8.57 - {manager = manager, timeout_heap = timeout_heap, active = active,
8.58 - canceling = canceling, messages = messages, store = store}
8.59 -
8.60 -val global_state = Synchronized.var "async_manager"
8.61 - (make_state NONE Thread_Heap.empty [] [] [] []);
8.62 -
8.63 -
8.64 -(* unregister thread *)
8.65 -
8.66 -fun unregister message thread =
8.67 - Synchronized.change global_state
8.68 - (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
8.69 - (case lookup_thread active thread of
8.70 - SOME (tool, _, _, desc) =>
8.71 - let
8.72 - val active' = delete_thread thread active;
8.73 - val now = Time.now ()
8.74 - val canceling' = (thread, (tool, now, desc)) :: canceling
8.75 - val message' = desc ^ "\n" ^ message
8.76 - val messages' = (tool, message') :: messages;
8.77 - val store' = (tool, message') ::
8.78 - (if length store <= message_store_limit then store
8.79 - else #1 (chop message_store_limit store));
8.80 - in make_state manager timeout_heap active' canceling' messages' store' end
8.81 - | NONE => state));
8.82 -
8.83 -
8.84 -(* main manager thread -- only one may exist *)
8.85 -
8.86 -val min_wait_time = seconds 0.3;
8.87 -val max_wait_time = seconds 10.0;
8.88 -
8.89 -fun replace_all bef aft =
8.90 - let
8.91 - fun aux seen "" = String.implode (rev seen)
8.92 - | aux seen s =
8.93 - if String.isPrefix bef s then
8.94 - aux seen "" ^ aft ^ aux [] (unprefix bef s)
8.95 - else
8.96 - aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
8.97 - in aux [] end
8.98 -
8.99 -(* This is a workaround for Proof General's off-by-a-few sendback display bug,
8.100 - whereby "pr" in "proof" is not highlighted. *)
8.101 -val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
8.102 -
8.103 -fun print_new_messages () =
8.104 - case Synchronized.change_result global_state
8.105 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
8.106 - (messages, make_state manager timeout_heap active canceling []
8.107 - store)) of
8.108 - [] => ()
8.109 - | msgs as (tool, _) :: _ =>
8.110 - let val ss = break_into_chunks (map snd msgs) in
8.111 - List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
8.112 - end
8.113 -
8.114 -fun check_thread_manager () = Synchronized.change global_state
8.115 - (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
8.116 - if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
8.117 - else let val manager = SOME (Toplevel.thread false (fn () =>
8.118 - let
8.119 - fun time_limit timeout_heap =
8.120 - (case try Thread_Heap.min timeout_heap of
8.121 - NONE => Time.+ (Time.now (), max_wait_time)
8.122 - | SOME (time, _) => time);
8.123 -
8.124 - (*action: find threads whose timeout is reached, and interrupt canceling threads*)
8.125 - fun action {manager, timeout_heap, active, canceling, messages, store} =
8.126 - let val (timeout_threads, timeout_heap') =
8.127 - Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
8.128 - in
8.129 - if null timeout_threads andalso null canceling then
8.130 - NONE
8.131 - else
8.132 - let
8.133 - val _ = List.app (Simple_Thread.interrupt o #1) canceling
8.134 - val canceling' = filter (Thread.isActive o #1) canceling
8.135 - val state' = make_state manager timeout_heap' active canceling' messages store;
8.136 - in SOME (map #2 timeout_threads, state') end
8.137 - end;
8.138 - in
8.139 - while Synchronized.change_result global_state
8.140 - (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
8.141 - if null active andalso null canceling andalso null messages
8.142 - then (false, make_state NONE timeout_heap active canceling messages store)
8.143 - else (true, state))
8.144 - do
8.145 - (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
8.146 - |> these
8.147 - |> List.app (unregister "Timed out.\n");
8.148 - print_new_messages ();
8.149 - (*give threads some time to respond to interrupt*)
8.150 - OS.Process.sleep min_wait_time)
8.151 - end))
8.152 - in make_state manager timeout_heap active canceling messages store end)
8.153 -
8.154 -
8.155 -(* register thread *)
8.156 -
8.157 -fun register tool birth_time death_time desc thread =
8.158 - (Synchronized.change global_state
8.159 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
8.160 - let
8.161 - val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
8.162 - val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
8.163 - val state' = make_state manager timeout_heap' active' canceling messages store;
8.164 - in state' end);
8.165 - check_thread_manager ())
8.166 -
8.167 -
8.168 -fun launch tool birth_time death_time desc f =
8.169 - (Toplevel.thread true
8.170 - (fn () =>
8.171 - let
8.172 - val self = Thread.self ()
8.173 - val _ = register tool birth_time death_time desc self
8.174 - val message = f ()
8.175 - in unregister message self end);
8.176 - ())
8.177 -
8.178 -
8.179 -(** user commands **)
8.180 -
8.181 -(* kill threads *)
8.182 -
8.183 -fun kill_threads tool workers = Synchronized.change global_state
8.184 - (fn {manager, timeout_heap, active, canceling, messages, store} =>
8.185 - let
8.186 - val killing =
8.187 - map_filter (fn (th, (tool', _, _, desc)) =>
8.188 - if tool' = tool then SOME (th, (tool', Time.now (), desc))
8.189 - else NONE) active
8.190 - val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
8.191 - val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
8.192 - in state' end);
8.193 -
8.194 -
8.195 -(* running threads *)
8.196 -
8.197 -fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
8.198 -
8.199 -fun running_threads tool workers =
8.200 - let
8.201 - val {active, canceling, ...} = Synchronized.value global_state;
8.202 -
8.203 - val now = Time.now ();
8.204 - fun running_info (_, (tool', birth_time, death_time, desc)) =
8.205 - if tool' = tool then
8.206 - SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
8.207 - seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
8.208 - else
8.209 - NONE
8.210 - fun canceling_info (_, (tool', death_time, desc)) =
8.211 - if tool' = tool then
8.212 - SOME ("Trying to interrupt thread since " ^
8.213 - seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
8.214 - else
8.215 - NONE
8.216 - val running =
8.217 - case map_filter running_info active of
8.218 - [] => ["No " ^ workers ^ " running."]
8.219 - | ss => "Running " ^ workers ^ ":" :: ss
8.220 - val interrupting =
8.221 - case map_filter canceling_info canceling of
8.222 - [] => []
8.223 - | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
8.224 - in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
8.225 -
8.226 -fun thread_messages tool worker opt_limit =
8.227 - let
8.228 - val limit = the_default message_display_limit opt_limit;
8.229 - val tool_store = Synchronized.value global_state
8.230 - |> #store |> filter (curry (op =) tool o fst)
8.231 - val header =
8.232 - "Recent " ^ worker ^ " messages" ^
8.233 - (if length tool_store <= limit then ":"
8.234 - else " (" ^ string_of_int limit ^ " displayed):");
8.235 - in
8.236 - List.app Output.urgent_message (header :: break_into_chunks
8.237 - (map snd (#1 (chop limit tool_store))))
8.238 - end
8.239 -
8.240 -end;
9.1 --- a/src/HOL/Tools/try.ML Tue Dec 07 10:03:43 2010 +0100
9.2 +++ b/src/HOL/Tools/try.ML Tue Dec 07 11:50:16 2010 +0100
9.3 @@ -77,28 +77,33 @@
9.4 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
9.5
9.6 fun do_try auto timeout_opt st =
9.7 - case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
9.8 - |> map_filter I |> sort (int_ord o pairself snd) of
9.9 - [] => (if auto then () else writeln "No proof found."; (false, st))
9.10 - | xs as (s, _) :: _ =>
9.11 - let
9.12 - val xs = xs |> map swap |> AList.coalesce (op =)
9.13 - |> map (swap o apsnd commas)
9.14 - val message =
9.15 - (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
9.16 - Markup.markup Markup.sendback
9.17 - ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
9.18 - " " ^ s) ^
9.19 - "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
9.20 - in
9.21 - (true, st |> (if auto then
9.22 - Proof.goal_message
9.23 - (fn () => Pretty.chunks [Pretty.str "",
9.24 - Pretty.markup Markup.hilite
9.25 - [Pretty.str message]])
9.26 - else
9.27 - tap (fn _ => Output.urgent_message message)))
9.28 - end
9.29 + let
9.30 + val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
9.31 + in
9.32 + case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
9.33 + |> map_filter I |> sort (int_ord o pairself snd) of
9.34 + [] => (if auto then () else writeln "No proof found."; (false, st))
9.35 + | xs as (s, _) :: _ =>
9.36 + let
9.37 + val xs = xs |> map swap |> AList.coalesce (op =)
9.38 + |> map (swap o apsnd commas)
9.39 + val message =
9.40 + (if auto then "Auto Try found a proof" else "Try this command") ^
9.41 + ": " ^
9.42 + Markup.markup Markup.sendback
9.43 + ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
9.44 + else "apply") ^ " " ^ s) ^
9.45 + "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
9.46 + in
9.47 + (true, st |> (if auto then
9.48 + Proof.goal_message
9.49 + (fn () => Pretty.chunks [Pretty.str "",
9.50 + Pretty.markup Markup.hilite
9.51 + [Pretty.str message]])
9.52 + else
9.53 + tap (fn _ => Output.urgent_message message)))
9.54 + end
9.55 + end
9.56
9.57 val invoke_try = fst oo do_try false
9.58