Admin/isatest-makeall
author kleing
Fri Apr 25 15:17:36 2003 +0200 (2003-04-25)
changeset 13924 09f6f2fefb25
parent 13901 af38553e61ee
child 13962 908f6776a59b
permissions -rwxr-xr-x
no need to be nice everywhere
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@13838
    11
MAILTO="kleing@in.tum.de nipkow@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
kleing@13924
    54
NICE=nice
kleing@13924
    55
isatest@13838
    56
case $HOSTNAME in
isatest@13838
    57
        atbroy51)
isatest@13838
    58
	MFLAGS="-j 2"
isatest@13838
    59
	# MFLAGS=""
kleing@13924
    60
  NICE=""
isatest@13838
    61
	;;
isatest@13838
    62
isatest@13838
    63
        atbroy31)
isatest@13838
    64
        MFLAGS="-j 5"
isatest@13838
    65
        ;;
isatest@13838
    66
	
isatest@13838
    67
	atbroy12)
isatest@13838
    68
	MFLAGS="-j 5"
isatest@13838
    69
	;;
isatest@13838
    70
isatest@13838
    71
	sunbroy2)
isatest@13838
    72
	MFLAGS="-j 4"
isatest@13838
    73
	;;
isatest@13838
    74
kleing@13901
    75
	sunbroy1)
kleing@13901
    76
	MFLAGS="-j 2"
kleing@13901
    77
	;;
kleing@13901
    78
isatest@13838
    79
   	*)
isatest@13838
    80
	MFLAGS=""
isatest@13838
    81
        ;;
isatest@13838
    82
esac
isatest@13838
    83
isatest@13838
    84
isatest@13838
    85
isatest@13320
    86
LOGS=""
isatest@13320
    87
kleing@13231
    88
for SETTINGS in $@; do
kleing@13231
    89
kleing@13231
    90
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
kleing@13231
    91
    
kleing@13231
    92
kleing@13231
    93
    # logfile setup
kleing@13231
    94
isatest@13432
    95
    DATE=$(date "+%Y-%m-%d")
kleing@13231
    96
    SHORT=${SETTINGS##*/}
kleing@13231
    97
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
kleing@13231
    98
kleing@13231
    99
    # the test
kleing@13231
   100
kleing@13231
   101
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
kleing@13231
   102
kleing@13233
   103
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
kleing@13924
   104
    $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
kleing@13231
   105
kleing@13231
   106
    if [ $? -eq 0 ]
kleing@13231
   107
    then
isatest@13236
   108
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13231
   109
        gzip -f $TESTLOG
isatest@13246
   110
	rm -rf ~/isabelle-$SHORT
kleing@13231
   111
    else
kleing@13231
   112
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
isatest@13236
   113
	FAIL="$FAIL$SHORT "
isatest@13432
   114
	LOGS="${LOGS}$TESTLOG "
kleing@13231
   115
    fi
kleing@13231
   116
kleing@13231
   117
done
kleing@13231
   118
isatest@13236
   119
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
isatest@13236
   120
isatest@13236
   121
if [ "$FAIL" != "" ]; then
isatest@13236
   122
	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13320
   123
	
isatest@13320
   124
	echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP
isatest@13432
   125
	for L in $LOGS; do 
isatest@13432
   126
		echo "$HOSTNAME:$L" >> $TMP 
isatest@13432
   127
		echo "[...]" >> $TMP
isatest@13432
   128
		tail -3 $L >> $TMP
isatest@13432
   129
		echo >> $TMP
isatest@13432
   130
	done
isatest@13432
   131
	echo "Have a nice day," >> $TMP
isatest@13432
   132
	echo "  isatest" >> $TMP
isatest@13320
   133
isatest@13320
   134
        for R in $MAILTO; do
isatest@13320
   135
	    $MAIL "isabelle test failed" $R $TMP
isatest@13320
   136
	done
isatest@13320
   137
isatest@13320
   138
	rm $TMP
isatest@13320
   139
isatest@13236
   140
	exit 1
isatest@13236
   141
else
isatest@13236
   142
        echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13236
   143
fi
isatest@13236
   144
isatest@13236
   145
# end