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