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