Admin/isatest-makeall
author isatest
Fri Jun 21 15:39:19 2002 +0200 (2002-06-21)
changeset 13236 568bc754d303
parent 13233 5ab7bac534c9
child 13246 e51efc2029e9
permissions -rwxr-xr-x
included masterlog file
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
kleing@13232
    11
LOGPREFIX=~/log
kleing@13231
    12
isatest@13236
    13
MASTERLOG=$LOGPREFIX/isatest.log
isatest@13236
    14
kleing@13231
    15
## diagnostics
kleing@13231
    16
kleing@13231
    17
PRG="$(basename "$0")"
kleing@13231
    18
kleing@13231
    19
function usage()
kleing@13231
    20
{
kleing@13231
    21
  echo
kleing@13231
    22
  echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
kleing@13231
    23
  echo
kleing@13231
    24
  echo "  Run isatool makeall from specified distribution and settings."
kleing@13231
    25
  echo "  Send email if it fails."
kleing@13231
    26
  echo
kleing@13231
    27
  exit 1
kleing@13231
    28
}
kleing@13231
    29
kleing@13231
    30
function fail()
kleing@13231
    31
{
kleing@13231
    32
  echo "$1" >&2
kleing@13231
    33
  exit 2
kleing@13231
    34
}
kleing@13231
    35
kleing@13231
    36
## main
kleing@13231
    37
kleing@13231
    38
# argument checking
kleing@13231
    39
kleing@13231
    40
[ "$1" = "-?" ] && usage
kleing@13231
    41
[ "$#" -lt "2" ] && usage
kleing@13231
    42
kleing@13231
    43
DISTPREFIX=$1
kleing@13231
    44
shift
kleing@13231
    45
kleing@13231
    46
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
kleing@13231
    47
kleing@13231
    48
for SETTINGS in $@; do
kleing@13231
    49
kleing@13231
    50
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
kleing@13231
    51
    
kleing@13231
    52
kleing@13231
    53
    # logfile setup
kleing@13231
    54
kleing@13231
    55
    DATE=$(date "+%d-%b-%Y")
kleing@13231
    56
    SHORT=${SETTINGS##*/}
kleing@13231
    57
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
kleing@13231
    58
kleing@13231
    59
    # the test
kleing@13231
    60
kleing@13231
    61
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
kleing@13231
    62
kleing@13233
    63
    cp $DISTPREFIX/Isabelle/etc/settings $DISTPREFIX/Isabelle/etc/settings.save-$SHORT
kleing@13233
    64
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
kleing@13231
    65
    $DISTPREFIX/Isabelle/bin/isatool makeall all >> $TESTLOG 2>&1 
kleing@13231
    66
kleing@13231
    67
    if [ $? -eq 0 ]
kleing@13231
    68
    then
isatest@13236
    69
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
isatest@13236
    70
        mv $DISTPREFIX/Isabelle/etc/settings.save-$SHORT $DISTPREFIX/Isabelle/etc/settings
kleing@13231
    71
        gzip -f $TESTLOG
kleing@13231
    72
    else
kleing@13231
    73
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
isatest@13236
    74
	FAIL="$FAIL$SHORT "
kleing@13231
    75
        # more action here
kleing@13231
    76
    fi
kleing@13231
    77
kleing@13231
    78
done
kleing@13231
    79
isatest@13236
    80
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
isatest@13236
    81
isatest@13236
    82
if [ "$FAIL" != "" ]; then
isatest@13236
    83
	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13236
    84
	exit 1
isatest@13236
    85
else
isatest@13236
    86
        echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13236
    87
fi
isatest@13236
    88
isatest@13236
    89
# end