Admin/isatest-check

only make development snapshots for successful tests

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


## global settings

# send mail to:
MAILTO="[e-mail] [e-mail] [e-mail] [e-mail] [e-mail]"

ADMIN="[e-mail]"

# 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
ERRORLOG=$HOME/var/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
        $MAIL "isabelle test failed" $R $TMP
    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