Admin/isatest-check
author wenzelm
Thu, 01 Sep 2005 22:49:18 +0200
changeset 17226 0687c76021c0
parent 16559 2916415680b9
child 17847 5d5cada76409
permissions -rwxr-xr-x
refrain from sorting output;
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
16095
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts
kleing
parents: 15937
diff changeset
     9
## global settings
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts
kleing
parents: 15937
diff changeset
    10
. ~/admin/isatest-settings
13986
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
# mail program
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    17
MAIL=$HOME/bin/pmail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    18
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    19
# tmp file for sending mail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    20
TMP=/tmp/isatest-makedist.$$
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    21
16095
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts
kleing
parents: 15937
diff changeset
    22
export DISTPREFIX
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts
kleing
parents: 15937
diff changeset
    23
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    24
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    25
## diagnostics
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    26
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    27
PRG="$(basename "$0")"
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
function usage()
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    30
{
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    31
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    32
  echo "Usage: $PRG"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    33
  echo
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    34
  echo "   sends email for failed tests, checks for error.log,"
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    35
  echo "   generates development snapshot if test ok."
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    36
  echo "   To be called by cron."
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    37
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    38
  exit 1
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
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    41
function fail()
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
  echo "$1" >&2
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    44
  exit 2
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
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    47
## main
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    48
16559
2916415680b9 shortened time out by 3h (gives up at 12:00h now).
kleing
parents: 16507
diff changeset
    49
# check if tests are still running, wait for them to finish for max 5h
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    50
i=0
16559
2916415680b9 shortened time out by 3h (gives up at 12:00h now).
kleing
parents: 16507
diff changeset
    51
while [ -n "$(ls $RUNNING)" -a $i -lt 5 ]; do 
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    52
    sleep 3600
13992
kleing
parents: 13991
diff changeset
    53
    let "i = i+1"
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    54
done
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
# still running -> give up
13992
kleing
parents: 13991
diff changeset
    57
if [ -n "$(ls $RUNNING)" ]; then
16178
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    58
    echo "Giving up waiting for test to finish at $(date)." > $TMP
16507
ee552def8721 fix 'give up waiting message' (logs of running processes are not attached)
kleing
parents: 16362
diff changeset
    59
    echo "Attaching all error logs collected so far." >> $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    60
    echo >> $TMP
16178
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    61
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    62
    if [ -e $ERRORLOG ]; then
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    63
        cat $ERRORLOG >> $TMP
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    64
    fi
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    65
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    66
    echo "Have a nice day," >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    67
    echo "  isatest" >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    68
16178
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    69
    for R in $MAILTO; do
754efc5afd5d reduced timeout, send logs also when test taking too long
kleing
parents: 16095
diff changeset
    70
        LOGS=$ERRORDIR/isatest*.log
16362
f321def7279c fixed spelling;
wenzelm
parents: 16178
diff changeset
    71
        $MAIL "isabelle test taking too long" $R $TMP $LOGS
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    72
    done
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    73
    
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    74
    exit 1
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    75
fi
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
# no tests running, check if there were errors
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    78
if [ -e $ERRORLOG ]; then
13992
kleing
parents: 13991
diff changeset
    79
    cat $ERRORLOG > $TMP
kleing
parents: 13991
diff changeset
    80
    echo "Have a nice day," >> $TMP
kleing
parents: 13991
diff changeset
    81
    echo "  isatest" >> $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    82
13992
kleing
parents: 13991
diff changeset
    83
    for R in $MAILTO; do
14038
afeaca7d943a attach log files
kleing
parents: 14035
diff changeset
    84
        LOGS=$ERRORDIR/isatest*.log
14039
bb70604a07c4 fix typo
kleing
parents: 14038
diff changeset
    85
        $MAIL "isabelle test failed" $R $TMP $LOGS
13992
kleing
parents: 13991
diff changeset
    86
    done
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    87
13992
kleing
parents: 13991
diff changeset
    88
    rm $TMP
kleing
parents: 13991
diff changeset
    89
    exit 1
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    90
fi
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    91
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    92
# generate development snapshot page only for successful tests
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    93
(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
    94
echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    95
13992
kleing
parents: 13991
diff changeset
    96
exit 0
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    97
## end