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