Admin/isatest-makeall
author isatest
Tue Jul 30 10:29:34 2002 +0200 (2002-07-30)
changeset 13432 470daa444967
parent 13359 982827aacb39
child 13838 fe83f2231767
permissions -rwxr-xr-x
- changed date format for proper lexicographical ordering
- send tail of log in email
kleing@13231
     1
#!/usr/bin/env bash
kleing@13231
     2
#
kleing@13231
     3
# $Id$
kleing@13231
     4
# Author: Gerwin Klein, TU Muenchen
kleing@13231
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
kleing@13231
     6
#
kleing@13231
     7
# DESCRIPTION: Run isatool makeall from specified distribution and settings.
kleing@13231
     8
#              Send email if it fails.
kleing@13231
     9
kleing@13231
    10
## global settings
isatest@13359
    11
MAILTO="kleing@in.tum.de nipkow@in.tum.de wenzelm@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
isatest@13246
    12
kleing@13232
    13
LOGPREFIX=~/log
kleing@13231
    14
isatest@13236
    15
MASTERLOG=$LOGPREFIX/isatest.log
isatest@13236
    16
isatest@13320
    17
TMP=/tmp/isatest-makeall.$$
isatest@13320
    18
isatest@13320
    19
MAIL=~/bin/pmail
isatest@13320
    20
kleing@13231
    21
## diagnostics
kleing@13231
    22
kleing@13231
    23
PRG="$(basename "$0")"
kleing@13231
    24
kleing@13231
    25
function usage()
kleing@13231
    26
{
kleing@13231
    27
  echo
kleing@13231
    28
  echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
kleing@13231
    29
  echo
kleing@13231
    30
  echo "  Run isatool makeall from specified distribution and settings."
kleing@13231
    31
  echo "  Send email if it fails."
kleing@13231
    32
  echo
kleing@13231
    33
  exit 1
kleing@13231
    34
}
kleing@13231
    35
kleing@13231
    36
function fail()
kleing@13231
    37
{
kleing@13231
    38
  echo "$1" >&2
kleing@13231
    39
  exit 2
kleing@13231
    40
}
kleing@13231
    41
kleing@13231
    42
## main
kleing@13231
    43
kleing@13231
    44
# argument checking
kleing@13231
    45
kleing@13231
    46
[ "$1" = "-?" ] && usage
kleing@13231
    47
[ "$#" -lt "2" ] && usage
kleing@13231
    48
kleing@13231
    49
DISTPREFIX=$1
kleing@13231
    50
shift
kleing@13231
    51
kleing@13231
    52
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
kleing@13231
    53
isatest@13320
    54
LOGS=""
isatest@13320
    55
kleing@13231
    56
for SETTINGS in $@; do
kleing@13231
    57
kleing@13231
    58
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
kleing@13231
    59
    
kleing@13231
    60
kleing@13231
    61
    # logfile setup
kleing@13231
    62
isatest@13432
    63
    DATE=$(date "+%Y-%m-%d")
kleing@13231
    64
    SHORT=${SETTINGS##*/}
kleing@13231
    65
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
kleing@13231
    66
kleing@13231
    67
    # the test
kleing@13231
    68
kleing@13231
    69
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
kleing@13231
    70
kleing@13233
    71
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
isatest@13320
    72
    nice $DISTPREFIX/Isabelle/bin/isatool makeall -j 2 all >> $TESTLOG 2>&1 
kleing@13231
    73
kleing@13231
    74
    if [ $? -eq 0 ]
kleing@13231
    75
    then
isatest@13236
    76
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13231
    77
        gzip -f $TESTLOG
isatest@13246
    78
	rm -rf ~/isabelle-$SHORT
kleing@13231
    79
    else
kleing@13231
    80
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
isatest@13236
    81
	FAIL="$FAIL$SHORT "
isatest@13432
    82
	LOGS="${LOGS}$TESTLOG "
kleing@13231
    83
    fi
kleing@13231
    84
kleing@13231
    85
done
kleing@13231
    86
isatest@13236
    87
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
isatest@13236
    88
isatest@13236
    89
if [ "$FAIL" != "" ]; then
isatest@13236
    90
	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13320
    91
	
isatest@13320
    92
	echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP
isatest@13432
    93
	for L in $LOGS; do 
isatest@13432
    94
		echo "$HOSTNAME:$L" >> $TMP 
isatest@13432
    95
		echo "[...]" >> $TMP
isatest@13432
    96
		tail -3 $L >> $TMP
isatest@13432
    97
		echo >> $TMP
isatest@13432
    98
	done
isatest@13432
    99
	echo "Have a nice day," >> $TMP
isatest@13432
   100
	echo "  isatest" >> $TMP
isatest@13320
   101
isatest@13320
   102
        for R in $MAILTO; do
isatest@13320
   103
	    $MAIL "isabelle test failed" $R $TMP
isatest@13320
   104
	done
isatest@13320
   105
isatest@13320
   106
	rm $TMP
isatest@13320
   107
isatest@13236
   108
	exit 1
isatest@13236
   109
else
isatest@13236
   110
        echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13236
   111
fi
isatest@13236
   112
isatest@13236
   113
# end