--- 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