#!/usr/bin/env bash
#
# $Id$
# Author: Gerwin Klein, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: sends email for failed tests, checks for error.log,
# generates development snapshot if test ok
# source bashrc, we're called by cron
. ~/.bashrc
# produce empty list for patterns like isatest-*.log if no
# such file exists
shopt -s nullglob
## global settings
# send mail to:
MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk skalberg@in.tum.de"
ADMIN="berghofe@in.tum.de"
# canoncical home for all platforms
HOME=/usr/stud/isatest
# where to find the distribution
DISTPREFIX=$HOME/isadist
# mail program
MAIL=$HOME/bin/pmail
# where the logs are
ERRORDIR=$HOME/var
ERRORLOG=$ERRORDIR/error.log
MASTERLOG=$HOME/log/isatest.log
# where the test-still-running files are
RUNNING=$HOME/var/running
# tmp file for sending mail
TMP=/tmp/isatest-makedist.$$
## 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 to finish for max 10h
i=0
while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do
sleep 3600
let "i = i+1"
done
# still running -> give up
if [ -n "$(ls $RUNNING)" ]; then
echo "giving up waiting for test to finish at $(date)" > $TMP
echo >> $TMP
echo "Have a nice day," >> $TMP
echo " isatest" >> $TMP
for R in $ADMIN; do
$MAIL "isabelle test taking to long" $R $TMP
done
exit 1
fi
# no tests running, check if there were errors
if [ -e $ERRORLOG ]; then
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
exit 1
fi
# generate development snapshot page only for successful tests
(cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
exit 0
## end