Admin/isatest-check
author kleing
Fri, 27 May 2005 01:09:44 +0200
changeset 16095 f6af6b265d20
parent 15937 b74dfcdeac1b
child 16178 754efc5afd5d
permissions -rwxr-xr-x
put global isatest settings in one file, sourced by the other scripts
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
16095
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts
kleing
parents: 15937
diff changeset
    16
ADMIN="berghofe@in.tum.de kleing@in.tum.de"
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    17
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    18
# mail program
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    19
MAIL=$HOME/bin/pmail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    20
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    21
# tmp file for sending mail
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    22
TMP=/tmp/isatest-makedist.$$
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    23
16095
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts
kleing
parents: 15937
diff changeset
    24
export DISTPREFIX
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts
kleing
parents: 15937
diff changeset
    25
13986
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
## diagnostics
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
PRG="$(basename "$0")"
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
function usage()
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    32
{
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    33
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    34
  echo "Usage: $PRG"
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    35
  echo
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    36
  echo "   sends email for failed tests, checks for error.log,"
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    37
  echo "   generates development snapshot if test ok."
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    38
  echo "   To be called by cron."
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    39
  echo
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    40
  exit 1
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
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    43
function fail()
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    44
{
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    45
  echo "$1" >&2
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    46
  exit 2
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
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    49
## main
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
# 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
    52
i=0
13992
kleing
parents: 13991
diff changeset
    53
while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do 
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    54
    sleep 3600
13992
kleing
parents: 13991
diff changeset
    55
    let "i = i+1"
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    56
done
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    57
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    58
# still running -> give up
13992
kleing
parents: 13991
diff changeset
    59
if [ -n "$(ls $RUNNING)" ]; then
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    60
    echo "giving up waiting for test to finish at $(date)" > $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    61
    echo >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    62
    echo "Have a nice day," >> $TMP
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    63
    echo "  isatest" >> $TMP
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
    for R in $ADMIN; do
13989
kleing
parents: 13986
diff changeset
    66
        $MAIL "isabelle test taking to long" $R $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    67
    done
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    68
    
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    69
    exit 1
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    70
fi
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    71
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    72
# no tests running, check if there were errors
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    73
if [ -e $ERRORLOG ]; then
13992
kleing
parents: 13991
diff changeset
    74
    cat $ERRORLOG > $TMP
kleing
parents: 13991
diff changeset
    75
    echo "Have a nice day," >> $TMP
kleing
parents: 13991
diff changeset
    76
    echo "  isatest" >> $TMP
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    77
13992
kleing
parents: 13991
diff changeset
    78
    for R in $MAILTO; do
14038
afeaca7d943a attach log files
kleing
parents: 14035
diff changeset
    79
        LOGS=$ERRORDIR/isatest*.log
14039
bb70604a07c4 fix typo
kleing
parents: 14038
diff changeset
    80
        $MAIL "isabelle test failed" $R $TMP $LOGS
13992
kleing
parents: 13991
diff changeset
    81
    done
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    82
13992
kleing
parents: 13991
diff changeset
    83
    rm $TMP
kleing
parents: 13991
diff changeset
    84
    exit 1
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    85
fi
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    86
13993
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    87
# generate development snapshot page only for successful tests
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    88
(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
    89
echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
88a8911bb65d only make development snapshots for successful tests
kleing
parents: 13992
diff changeset
    90
13992
kleing
parents: 13991
diff changeset
    91
exit 0
13986
d2fd7deceaa6 check for error log, send mail if exists
kleing
parents:
diff changeset
    92
## end