Admin/isatest-check
author kleing
Fri, 09 May 2003 14:08:04 +0200
changeset 13992 93769c6c85d7
parent 13991 b289ab046d3b
child 13993 88a8911bb65d
permissions -rwxr-xr-x
fixes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     1
#!/usr/bin/env bash
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     2
#
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     3
# $Id$
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     4
# Author: Gerwin Klein, TU Muenchen
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     6
#
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     7
# DESCRIPTION: sends email for failed tests (checks for error.log)
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     8
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
     9
# source bashrc, we're called by cron
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    10
. ~/.bashrc
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    11
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    12
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    13
## global settings
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    14
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    15
# send mail to:
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    16
MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    17
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    18
ADMIN="kleing@in.tum.de"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    19
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    20
# canoncical home for all platforms
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    21
HOME=/usr/stud/isatest
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    22
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    23
# mail program
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    24
MAIL=$HOME/bin/pmail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    25
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    26
# where the error log is
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    27
ERRORLOG=$HOME/var/error.log
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    28
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    29
# where the test-still-running files are
13991
b289ab046d3b var/run -> var/running
kleing
parents: 13989
diff changeset
    30
RUNNING=$HOME/var/running
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    31
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    32
# tmp file for sending mail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    33
TMP=/tmp/isatest-makedist.$$
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    34
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    35
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    36
## diagnostics
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    37
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    38
PRG="$(basename "$0")"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    39
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    40
function usage()
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    41
{
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    42
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    43
  echo "Usage: $PRG"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    44
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    45
  echo "   sends email for failed tests, checks for error.log."
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    46
  echo "   To be called by cron."
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    47
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    48
  exit 1
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    49
}
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    50
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    51
function fail()
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    52
{
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    53
  echo "$1" >&2
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    54
  exit 2
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    55
}
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    56
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    57
## main
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    58
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    59
# check if tests are still running, wait for them to finish for max 10h
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    60
i=0
13992
kleing
parents: 13991
diff changeset
    61
while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do 
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    62
    sleep 3600
13992
kleing
parents: 13991
diff changeset
    63
    let "i = i+1"
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    64
done
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    65
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    66
# still running -> give up
13992
kleing
parents: 13991
diff changeset
    67
if [ -n "$(ls $RUNNING)" ]; then
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    68
    echo "giving up waiting for test to finish at $(date)" > $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    69
    echo >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    70
    echo "Have a nice day," >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    71
    echo "  isatest" >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    72
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    73
    for R in $ADMIN; do
13989
kleing
parents: 13986
diff changeset
    74
        $MAIL "isabelle test taking to long" $R $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    75
    done
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    76
    
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    77
    exit 1
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    78
fi
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    79
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    80
# no tests running, check if there were errors
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    81
if [ -e $ERRORLOG ]; then
13992
kleing
parents: 13991
diff changeset
    82
    cat $ERRORLOG > $TMP
kleing
parents: 13991
diff changeset
    83
    echo "Have a nice day," >> $TMP
kleing
parents: 13991
diff changeset
    84
    echo "  isatest" >> $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    85
13992
kleing
parents: 13991
diff changeset
    86
    for R in $MAILTO; do
kleing
parents: 13991
diff changeset
    87
        $MAIL "isabelle test failed" $R $TMP
kleing
parents: 13991
diff changeset
    88
    done
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    89
13992
kleing
parents: 13991
diff changeset
    90
    rm $TMP
kleing
parents: 13991
diff changeset
    91
    exit 1
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    92
fi
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    93
13992
kleing
parents: 13991
diff changeset
    94
exit 0
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    95
## end