Admin/isatest-check
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 14170 edd5a2ea3807
child 15887 7dee3396d8b0
permissions -rwxr-xr-x
Merged in license change from Isabelle2004
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
#
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
     6
# DESCRIPTION: sends email for failed tests, checks for error.log,
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
     7
#              generates development snapshot if test ok
13986
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
14038
afeaca7d943a attach log files
kleing
parents: 14035
diff changeset
    12
# produce empty list for patterns like isatest-*.log if no 
afeaca7d943a attach log files
kleing
parents: 14035
diff changeset
    13
# such file exists 
afeaca7d943a attach log files
kleing
parents: 14035
diff changeset
    14
shopt -s nullglob
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    15
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    16
## global settings
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
# send mail to:
14170
edd5a2ea3807 Added skalberg to recepients, changed admin from kleing to berghofe.
skalberg
parents: 14039
diff changeset
    19
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"
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    20
14170
edd5a2ea3807 Added skalberg to recepients, changed admin from kleing to berghofe.
skalberg
parents: 14039
diff changeset
    21
ADMIN="berghofe@in.tum.de"
13986
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
# canoncical home for all platforms
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    24
HOME=/usr/stud/isatest
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    25
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    26
# where to find the distribution
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    27
DISTPREFIX=$HOME/isadist
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    28
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    29
# mail program
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    30
MAIL=$HOME/bin/pmail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    31
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    32
# where the logs are
14035
c46ce87960fb attach log files
kleing
parents: 13993
diff changeset
    33
ERRORDIR=$HOME/var
c46ce87960fb attach log files
kleing
parents: 13993
diff changeset
    34
ERRORLOG=$ERRORDIR/error.log
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    35
MASTERLOG=$HOME/log/isatest.log
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    36
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    37
# where the test-still-running files are
13991
b289ab046d3b var/run -> var/running
kleing
parents: 13989
diff changeset
    38
RUNNING=$HOME/var/running
13986
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
# tmp file for sending mail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    41
TMP=/tmp/isatest-makedist.$$
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    42
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    43
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    44
## diagnostics
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    45
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    46
PRG="$(basename "$0")"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    47
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    48
function usage()
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
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    51
  echo "Usage: $PRG"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    52
  echo
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    53
  echo "   sends email for failed tests, checks for error.log,"
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    54
  echo "   generates development snapshot if test ok."
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    55
  echo "   To be called by cron."
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    56
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    57
  exit 1
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
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    60
function fail()
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    61
{
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    62
  echo "$1" >&2
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    63
  exit 2
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    64
}
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
## main
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    67
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    68
# 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
    69
i=0
13992
kleing
parents: 13991
diff changeset
    70
while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do 
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    71
    sleep 3600
13992
kleing
parents: 13991
diff changeset
    72
    let "i = i+1"
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    73
done
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    74
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    75
# still running -> give up
13992
kleing
parents: 13991
diff changeset
    76
if [ -n "$(ls $RUNNING)" ]; then
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    77
    echo "giving up waiting for test to finish at $(date)" > $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    78
    echo >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    79
    echo "Have a nice day," >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    80
    echo "  isatest" >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    81
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    82
    for R in $ADMIN; do
13989
kleing
parents: 13986
diff changeset
    83
        $MAIL "isabelle test taking to long" $R $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    84
    done
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    85
    
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    86
    exit 1
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    87
fi
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    88
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    89
# no tests running, check if there were errors
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    90
if [ -e $ERRORLOG ]; then
13992
kleing
parents: 13991
diff changeset
    91
    cat $ERRORLOG > $TMP
kleing
parents: 13991
diff changeset
    92
    echo "Have a nice day," >> $TMP
kleing
parents: 13991
diff changeset
    93
    echo "  isatest" >> $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    94
13992
kleing
parents: 13991
diff changeset
    95
    for R in $MAILTO; do
14038
afeaca7d943a attach log files
kleing
parents: 14035
diff changeset
    96
        LOGS=$ERRORDIR/isatest*.log
14039
bb70604a07c4 fix typo
kleing
parents: 14038
diff changeset
    97
        $MAIL "isabelle test failed" $R $TMP $LOGS
13992
kleing
parents: 13991
diff changeset
    98
    done
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    99
13992
kleing
parents: 13991
diff changeset
   100
    rm $TMP
kleing
parents: 13991
diff changeset
   101
    exit 1
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
   102
fi
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
   103
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
   104
# generate development snapshot page only for successful tests
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
   105
(cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
   106
echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
   107
13992
kleing
parents: 13991
diff changeset
   108
exit 0
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
   109
## end