merged

--- a/Admin/isatest/isatest-makeall	Thu Sep 03 14:49:34 2009 +0200
+++ b/Admin/isatest/isatest-makeall	Thu Sep 03 14:50:02 2009 +0200
@@ -10,6 +10,8 @@
 # max time until test is aborted (in sec)
 MAXTIME=28800
 
+PUBLISH_TEST=/home/isabelle-repository/repos/testtool/publish_test.py
+
 ## diagnostics
 
 PRG="$(basename "$0")"
@@ -120,6 +122,8 @@
   TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
 fi
 
+IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")
+
 # main test loop
 
 log "starting [$@]"
@@ -159,10 +163,16 @@
     then
         # test log and cleanup
         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+        if [ -x $PUBLISH_TEST ]; then
+            $PUBLISH_TEST -r $IDENT -s "SUCCESS" -a log $TESTLOG
+        fi
         gzip -f $TESTLOG
     else
         # test log
         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+        if [ -x $PUBLISH_TEST ]; then
+             $PUBLISH_TEST -r $IDENT -s "FAIL" -a log $TESTLOG
+        fi
 
         # error log
         echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG

--- a/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 14:49:34 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 14:50:02 2009 +0200
@@ -1,1 +1,2 @@
-use_thy "MirabelleTest";
+if can (unprefix "polyml") (getenv "ML_SYSTEM") then use_thy "MirabelleTest"
+else ();

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 14:49:34 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 14:50:02 2009 +0200
@@ -70,13 +70,13 @@
 
 fun log_sep thy = log thy "------------------"
 
-fun try_with f NONE = SOME ()
-  | try_with f (SOME e) = (f e; try (fn () => reraise e) ())
+fun log_exn thy name (exn : exn) = log thy ("Unhandled exception in action " ^
+  quote name ^ ":\n" ^ PolyML.makestring exn)
 
-fun capture_exns thy name f x =
-  (case try_with I (Exn.get_exn (Exn.capture f x)) of
-    NONE => (log thy ("Unhandled exception in " ^ quote name); log_sep thy)
-  | SOME _ => log_sep thy)
+fun try_with f g x = SOME (g x)
+  handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; NONE)
+
+fun capture_exns thy name f x = (try_with (log_exn thy name) f x; log_sep thy)
 
 fun apply_actions thy info (pre, post, time) actions =
   let
@@ -112,12 +112,12 @@
 
 end
 
-val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
+val whitelist = ["apply", "by", "proof"]
 
 fun step_hook tr pre post =
  (* FIXME: might require wrapping into "interruptible" *)
   if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
-     not (member (op =) blacklist (Toplevel.name_of tr))
+     member (op =) whitelist (Toplevel.name_of tr)
   then basic_hook tr (Toplevel.proof_of pre) (SOME post)
   else ()   (* FIXME: add theory_hook here *)
 

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 03 14:49:34 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 03 14:50:02 2009 +0200
@@ -83,12 +83,14 @@
     fun timed_metis thms =
       uncurry with_time (Mirabelle.cpu_time apply_metis thms)
       handle TimeLimit.TimeOut => "time out"
-    fun log_metis s = log ("-----\nmetis (sledgehammer): " ^ s)
+           | ERROR msg => "error: " ^ msg
+    fun log_metis s = log ("metis (sledgehammer): " ^ s)
   in
     if not (AList.defined (op =) args metisK) then ()
     else if is_none thm_names then ()
     else
-      these thm_names
+      log "-----"
+      |> K (these thm_names)
       |> get_thms (Proof.context_of st)
       |> timed_metis
       |> log_metis