Admin/isatest-check

world map now transparent

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