# HG changeset patch
# User wenzelm
# Date 1229373660 -3600
# Node ID f2b45eea6dac8809bd52f4a4aff596cac5e6a07a
# Parent  d2b60c49a7133dcf1afd806109d17d4949820866
added 'atp_messages' command, which displays recent messages synchronously;

diff -r d2b60c49a713 -r f2b45eea6dac doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 10:19:02 2008 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Dec 15 21:41:00 2008 +0100
@@ -804,12 +804,14 @@
     @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+    @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{method_def (HOL) metis} & : & @{text method} \\
   \end{matharray}
 
   \begin{rail}
   'sledgehammer' (nameref *)
   ;
+  'atp\_messages' ('(' nat ')')?
 
   'metis' thmrefs
   ;
@@ -842,6 +844,12 @@
   \item @{command (HOL) atp_kill} terminates all presently running
   provers.
 
+  \item @{command (HOL) atp_messages} displays recent messages issued
+  by automated theorem provers.  This allows to examine results that
+  might have got lost due to the asynchronous nature of default
+  @{command (HOL) sledgehammer} output.  An optional message limit may
+  be specified (default 5).
+
   \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
   with the given facts.  Metis is an automated proof tool of medium
   strength, but is fully integrated into Isabelle/HOL, with explicit
diff -r d2b60c49a713 -r f2b45eea6dac src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Mon Dec 15 10:19:02 2008 +0100
+++ b/src/HOL/Tools/atp_manager.ML	Mon Dec 15 21:41:00 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/atp_manager.ML
-    ID:         $Id$
     Author:     Fabian Immler, TU Muenchen
 
 ATP threads are registered here.
@@ -19,6 +18,7 @@
   val set_timeout: int -> unit
   val kill: unit -> unit
   val info: unit -> unit
+  val messages: int option -> unit
   type prover = int -> Proof.state -> bool * string
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
@@ -30,6 +30,9 @@
 
 (** preferences **)
 
+val message_store_limit = 20;
+val message_display_limit = 5;
+
 local
 
 val atps = ref "e";
@@ -85,13 +88,14 @@
  {timeout_heap: ThreadHeap.T,
   oldest_heap: ThreadHeap.T,
   active: (Thread.thread * (Time.time * Time.time * string)) list,
-  cancelling: (Thread.thread * (Time.time * Time.time * string)) list};
+  cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
+  messages: string list};
 
-fun make_state timeout_heap oldest_heap active cancelling =
+fun make_state timeout_heap oldest_heap active cancelling messages =
   State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
-    active = active, cancelling = cancelling};
+    active = active, cancelling = cancelling, messages = messages};
 
-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 *)
@@ -103,7 +107,7 @@
 (* unregister thread from thread manager -- move to cancelling *)
 
 fun unregister (success, message) thread = Synchronized.change_result state
-  (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+  (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
     let
       val info = lookup_thread active thread
 
@@ -127,7 +131,11 @@
         | SOME (_, _, desc) => "Sledgehammer: " ^ desc ^ "\n" ^ message ^
           (if null group_threads then ""
            else "\nInterrupted " ^ string_of_int (length group_threads - 1) ^ " other group members")
-    in (message', make_state timeout_heap oldest_heap active'' cancelling'') end);
+
+      val messages' = message ::
+       (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);
 
 
 (* kill excessive atp threads *)
@@ -140,12 +148,13 @@
 
 fun kill_oldest () =
   let exception Unchanged in
-    Synchronized.change_result state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+    Synchronized.change_result state
+      (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
         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) end)
+          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages) end)
       |> (priority o unregister (false, "Interrupted (maximum number of ATPs exceeded)"))
     handle Unchanged => ()
   end;
@@ -175,7 +184,7 @@
         | 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}) =
+      fun action (State {timeout_heap, oldest_heap, active, cancelling, messages}) =
         let val (timeout_threads, timeout_heap') =
           ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
         in
@@ -185,7 +194,7 @@
             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'
+              val state' = make_state timeout_heap' oldest_heap active cancelling' messages
             in SOME (map #2 timeout_threads, state') end
         end
     in
@@ -203,12 +212,13 @@
 
 fun register birthtime deadtime (thread, desc) =
  (check_thread_manager ();
-  Synchronized.change state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
-    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 end));
+  Synchronized.change state
+    (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+      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));
 
 
 
@@ -217,16 +227,17 @@
 (* kill: move all threads to cancelling *)
 
 fun kill () = Synchronized.change state
-  (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+  (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
     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) end);
+    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages end);
 
 
-(* info: information on running threads *)
+(* ATP info *)
 
 fun info () =
   let
-    val State {timeout_heap, oldest_heap, active, cancelling} = Synchronized.value state
+    val State {active, cancelling, ...} = Synchronized.value state
+
     fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
         ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), birth_time))
         ^ " s  --  "
@@ -235,6 +246,7 @@
     fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
         ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), dead_time))
         ^ " s:\n" ^ desc
+
     val running =
       if null active then "No ATPs running."
       else space_implode "\n\n" ("Running ATPs:" :: map running_info active)
@@ -242,8 +254,17 @@
       if null cancelling then ""
       else space_implode "\n\n"
         ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling)
+
   in writeln (running ^ "\n" ^ interrupting) end;
 
+fun messages opt_limit =
+  let
+    val limit = the_default message_display_limit opt_limit;
+    val State {messages = msgs, ...} = Synchronized.value state
+    val header = "Recent ATP messages" ^
+      (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
+  in writeln (cat_lines (header :: "" :: #1 (chop limit msgs))) end;
+
 
 
 (** The Sledgehammer **)
@@ -322,6 +343,11 @@
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
 
 val _ =
+  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
+    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+
+val _ =
   OuterSyntax.improper_command "print_atps" "print external provers" K.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
       Toplevel.keep (print_provers o Toplevel.theory_of)));
@@ -329,7 +355,7 @@
 val _ =
   OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
     (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
-    Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
+      Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
 
 end;