# HG changeset patch # User immler@in.tum.de # Date 1232697974 -3600 # Node ID dc1257eaa4f2eb7dbcb3892c22aa7ec947ddeedb # Parent b36bcbc1be3a93b6b0c10ab2be5c68e4d0504ed7 moved all output to watcher-thread diff -r b36bcbc1be3a -r dc1257eaa4f2 src/HOL/Tools/atp_manager.ML --- a/src/HOL/Tools/atp_manager.ML Thu Jan 22 11:23:15 2009 +0100 +++ b/src/HOL/Tools/atp_manager.ML Fri Jan 23 09:06:14 2009 +0100 @@ -89,13 +89,14 @@ oldest_heap: ThreadHeap.T, active: (Thread.thread * (Time.time * Time.time * string)) list, cancelling: (Thread.thread * (Time.time * Time.time * string)) list, - messages: string list}; + messages: string list, + store: string list}; -fun make_state timeout_heap oldest_heap active cancelling messages = +fun make_state timeout_heap oldest_heap active cancelling messages store = State {timeout_heap = timeout_heap, oldest_heap = oldest_heap, - active = active, cancelling = cancelling, messages = messages}; + active = active, cancelling = cancelling, messages = messages, store = store}; -val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] []); +val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []); (* the managing thread *) @@ -106,31 +107,27 @@ (* unregister thread *) -fun unregister (success, message) thread = Synchronized.change_result state - (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages} => +fun unregister (success, message) thread = Synchronized.change state + (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages, store} => (case lookup_thread active thread of SOME (birthtime, _, description) => let val (group, active') = if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active else List.partition (fn (th, _) => Thread.equal (th, thread)) active - (* do not interrupt successful thread, as it needs to print out its message - (and terminates afterwards - see start_prover )*) - val group' = if success then delete_thread thread group else group val now = Time.now () val cancelling' = - fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group' cancelling + fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling - val msg = description ^ "\n" ^ message - val message' = "Sledgehammer: " ^ msg ^ + val message' = description ^ "\n" ^ message ^ (if length group <= 1 then "" else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members") - val messages' = msg :: - (if length messages <= message_store_limit then messages - else #1 (chop message_store_limit messages)) - in (message', make_state timeout_heap oldest_heap active' cancelling' messages') end - | NONE => ("", state))); + val store' = message' :: + (if length store <= message_store_limit then store + else #1 (chop message_store_limit store)) + in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end + | NONE =>state)); (* kill excessive atp threads *) @@ -144,13 +141,13 @@ fun kill_oldest () = let exception Unchanged in Synchronized.change_result state - (fn State {timeout_heap, oldest_heap, active, cancelling, messages} => + (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} => if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active) then raise Unchanged else let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap - in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages) end) - |> (priority o unregister (false, "Interrupted (maximum number of ATPs exceeded)")) + in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages store) end) + |> unregister (false, "Interrupted (maximum number of ATPs exceeded)") handle Unchanged => () end; @@ -162,6 +159,13 @@ end; +fun print_new_messages () = + let val to_print = Synchronized.change_result state + (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} => + (messages, make_state timeout_heap oldest_heap active cancelling [] store)) + in if null to_print then () + else priority ("Sledgehammer: " ^ (space_implode "\n\n" to_print)) end; + (* start a watching thread which runs forever -- only one may exist *) @@ -178,8 +182,8 @@ NONE => SOME (Time.+ (Time.now (), max_wait_time)) | SOME (time, _) => SOME time) - (* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *) - fun action (State {timeout_heap, oldest_heap, active, cancelling, messages}) = + (* action: find threads whose timeout is reached, and interrupt cancelling threads *) + fun action (State {timeout_heap, oldest_heap, active, cancelling, messages, store}) = let val (timeout_threads, timeout_heap') = ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap in @@ -189,15 +193,16 @@ let val _ = List.app (SimpleThread.interrupt o #1) cancelling val cancelling' = filter (Thread.isActive o #1) cancelling - val state' = make_state timeout_heap' oldest_heap active cancelling' messages + val state' = make_state timeout_heap' oldest_heap active cancelling' messages store in SOME (map #2 timeout_threads, state') end end in while true do (Synchronized.timed_access state time_limit action |> these - |> List.app (priority o unregister (false, "Interrupted (reached timeout)")); + |> List.app (unregister (false, "Interrupted (reached timeout)")); kill_excessive (); + print_new_messages (); (*give threads time to respond to interrupt*) OS.Process.sleep min_wait_time) end))); @@ -208,12 +213,12 @@ fun register birthtime deadtime (thread, desc) = (check_thread_manager (); Synchronized.change state - (fn State {timeout_heap, oldest_heap, active, cancelling, messages} => + (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} => let val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap val active' = update_thread (thread, (birthtime, deadtime, desc)) active - in make_state timeout_heap' oldest_heap' active' cancelling messages end)); + in make_state timeout_heap' oldest_heap' active' cancelling messages store end)); @@ -222,9 +227,9 @@ (* kill: move all threads to cancelling *) fun kill () = Synchronized.change state - (fn State {timeout_heap, oldest_heap, active, cancelling, messages} => + (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} => let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active - in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages end); + in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store end); (* ATP info *) @@ -255,7 +260,7 @@ fun messages opt_limit = let val limit = the_default message_display_limit opt_limit; - val State {messages = msgs, ...} = Synchronized.value state + val State {store = msgs, ...} = Synchronized.value state val header = "Recent ATP messages" ^ (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):"); in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end; @@ -307,7 +312,7 @@ => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis") | ERROR msg => (false, "Error: " ^ msg) - val _ = priority (unregister result (Thread.self ())) + val _ = unregister result (Thread.self ()) in () end handle Interrupt => ()) in () end);