Admin/isatest-makeall
author nipkow
Wed Aug 04 11:25:08 2004 +0200 (2004-08-04)
changeset 15106 e8cef6993701
parent 14981 e73f8140af78
child 15888 64533471eec4
permissions -rwxr-xr-x
aded comment
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
#
kleing@13231
     6
# DESCRIPTION: Run isatool makeall from specified distribution and settings.
kleing@13962
     7
kleing@13231
     8
## global settings
isatest@13246
     9
kleing@13985
    10
# canoncical home for all platforms 
kleing@13985
    11
HOME=/usr/stud/isatest
kleing@13985
    12
kleing@13985
    13
# where the log files are
kleing@13962
    14
LOGPREFIX=$HOME/log
isatest@13236
    15
MASTERLOG=$LOGPREFIX/isatest.log
kleing@14035
    16
ERRORDIR=$HOME/var
kleing@14035
    17
ERRORLOG=$ERRORDIR/error.log
isatest@13236
    18
kleing@13985
    19
# where to put test-is-running files
kleing@13985
    20
RUNNING=$HOME/var/running
isatest@13320
    21
isatest@13320
    22
kleing@13231
    23
## diagnostics
kleing@13231
    24
kleing@13231
    25
PRG="$(basename "$0")"
kleing@13231
    26
kleing@13231
    27
function usage()
kleing@13231
    28
{
kleing@13231
    29
  echo
kleing@13231
    30
  echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
kleing@13231
    31
  echo
kleing@13985
    32
  echo "  Runs isatool makeall from specified distribution and settings."
kleing@13985
    33
  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
kleing@13231
    34
  echo
kleing@13231
    35
  exit 1
kleing@13231
    36
}
kleing@13231
    37
kleing@13231
    38
function fail()
kleing@13231
    39
{
kleing@13231
    40
  echo "$1" >&2
kleing@13231
    41
  exit 2
kleing@13231
    42
}
kleing@13231
    43
kleing@13231
    44
## main
kleing@13231
    45
kleing@13231
    46
# argument checking
kleing@13231
    47
kleing@13231
    48
[ "$1" = "-?" ] && usage
kleing@13231
    49
[ "$#" -lt "2" ] && usage
kleing@13231
    50
kleing@13231
    51
DISTPREFIX=$1
kleing@13231
    52
shift
kleing@13231
    53
kleing@13231
    54
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
kleing@13231
    55
kleing@13985
    56
# make file flags and nice setup for different target platforms
isatest@13838
    57
case $HOSTNAME in
kleing@13985
    58
    atbroy51)
kleing@13985
    59
        # 2 processors
kleing@13985
    60
        MFLAGS="-j 2"
kleing@13985
    61
        # MFLAGS=""
kleing@13985
    62
        NICE=""
kleing@13985
    63
        ;;
isatest@13838
    64
kleing@13985
    65
    atbroy31)
kleing@13985
    66
        # cluster
isatest@13838
    67
        MFLAGS="-j 5"
isatest@13838
    68
        ;;
kleing@13985
    69
  
kleing@13985
    70
    sunbroy2)
kleing@13990
    71
        MFLAGS="-j 6"
kleing@14012
    72
	NICE="nice"
kleing@13985
    73
        ;;
kleing@13985
    74
kleing@13985
    75
    sunbroy1)
kleing@13985
    76
        MFLAGS="-j 2"
kleing@14012
    77
	NICE="nice"
kleing@13985
    78
        ;;
isatest@13838
    79
kleing@13985
    80
    macbroy*)
kleing@13985
    81
        MFLAGS=""
kleing@13985
    82
        NICE=""
kleing@13985
    83
        ;;
isatest@13838
    84
kleing@13985
    85
    *)
kleing@13985
    86
        MFLAGS=""
kleing@13985
    87
        # be nice by default
kleing@13985
    88
        NICE=nice
isatest@13838
    89
        ;;
isatest@13838
    90
esac
isatest@13838
    91
kleing@13985
    92
# main test loop
isatest@13320
    93
kleing@13231
    94
for SETTINGS in $@; do
kleing@13231
    95
kleing@13231
    96
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
kleing@13231
    97
kleing@13231
    98
    # logfile setup
kleing@13231
    99
isatest@13432
   100
    DATE=$(date "+%Y-%m-%d")
kleing@13231
   101
    SHORT=${SETTINGS##*/}
kleing@13231
   102
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
kleing@13231
   103
kleing@13231
   104
    # the test
kleing@13231
   105
kleing@13987
   106
    touch $RUNNING/$SHORT.running
kleing@13985
   107
kleing@13231
   108
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
kleing@13231
   109
kleing@13233
   110
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
kleing@13924
   111
    $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
kleing@13231
   112
kleing@13231
   113
    if [ $? -eq 0 ]
kleing@13231
   114
    then
kleing@13985
   115
        # test log and cleanup
isatest@13236
   116
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13231
   117
        gzip -f $TESTLOG
kleing@13231
   118
    else
kleing@13985
   119
        # test log
kleing@13231
   120
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13985
   121
kleing@13985
   122
        # error log
kleing@14035
   123
        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
kleing@13985
   124
        echo "[...]" >> $ERRORLOG
kleing@14035
   125
        tail -3 $TESTLOG >> $ERRORLOG
kleing@13985
   126
        echo >> $ERRORLOG
kleing@13985
   127
kleing@13985
   128
        FAIL="$FAIL$SHORT "
kleing@14035
   129
        (cd $ERRORDIR; ln -s $TESTLOG)
kleing@13231
   130
    fi
kleing@13231
   131
kleing@13987
   132
    rm -f $RUNNING/$SHORT.running
kleing@13231
   133
done
kleing@13231
   134
kleing@13985
   135
# time and success/failure to master log
isatest@13236
   136
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
isatest@13236
   137
kleing@13985
   138
if [ -z "$FAIL" ]; then
kleing@13985
   139
    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13236
   140
else
kleing@13985
   141
    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
kleing@13985
   142
    exit 1
isatest@13236
   143
fi
isatest@13236
   144
isatest@13236
   145
# end