Admin/isatest-check

Simplified version of Jia's filter. Now all constants are pooled, rather than
relevance being compared against separate clauses. Rejects are no longer noted,
and units cannot be added at the end.

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

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