diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-check
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-check	Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,105 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+#
+# DESCRIPTION: sends email for failed tests, checks for error.log,
+#              generates development snapshot if test ok
+
+## global settings
+. ~/admin/isatest-settings
+
+# produce empty list for patterns like isatest-*.log if no 
+# such file exists 
+shopt -s nullglob
+
+# mail program
+MAIL=$HOME/bin/pmail
+
+# tmp file for sending mail
+TMP=/tmp/isatest-makedist.$$
+
+export DISTPREFIX
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG"
+  echo
+  echo "   sends email for failed tests, checks for error.log,"
+  echo "   generates development snapshot if test ok."
+  echo "   To be called by cron."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+## main
+
+# check if tests are still running, wait for them a couple of hours
+i=0
+while [ -n "$(ls $RUNNING)" -a $i -lt 8 ]; do 
+    sleep 3600
+    let "i = i+1"
+done
+
+FAIL=0
+
+# still running -> give up
+if [ -n "$(ls $RUNNING)" ]; then
+    echo "Giving up waiting for test to finish at $(date)." > $TMP
+    echo >> $TMP
+    echo "Sessions still running:" >> $TMP
+    echo "$(ls $RUNNING)" >> $TMP
+    echo >> $TMP
+    echo "Attaching all error logs collected so far." >> $TMP
+    echo >> $TMP
+
+    if [ -e $ERRORLOG ]; then
+        cat $ERRORLOG >> $TMP
+    fi
+
+    echo "Have a nice day," >> $TMP
+    echo "  isatest" >> $TMP
+
+    for R in $MAILTO; do
+        LOGS=$ERRORDIR/isatest*.log
+        $MAIL "isabelle test taking too long" $R $TMP $LOGS
+    done
+
+    rm $TMP
+    
+    FAIL=1
+elif [ -e $ERRORLOG ]; then
+  # no tests running, check if there were errors
+    cat $ERRORLOG > $TMP
+    echo "Have a nice day," >> $TMP
+    echo "  isatest" >> $TMP
+
+    for R in $MAILTO; do
+        LOGS=$ERRORDIR/isatest*.log
+        $MAIL "isabelle test failed" $R $TMP $LOGS
+    done
+    
+    rm $TMP
+fi
+
+# generate development snapshot page only for successful tests
+# (failures in experimental sessions ok)
+if [ "$FAIL"=="0" -a "$(echo $ERRORDIR/isatest*[^e].log)" == "$(echo)" ]; then
+  (cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
+  echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
+fi
+
+exit 0
+## end