Admin/isatest-makeall
author kleing
Fri May 09 11:54:04 2003 +0200 (2003-05-09)
changeset 13987 31891dd8c04b
parent 13985 3852929a8d1d
child 13990 506102b6a6d4
permissions -rwxr-xr-x
tuned
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@13962
     8
kleing@13231
     9
## global settings
isatest@13246
    10
kleing@13985
    11
# canoncical home for all platforms 
kleing@13985
    12
HOME=/usr/stud/isatest
kleing@13985
    13
kleing@13985
    14
# where the log files are
kleing@13962
    15
LOGPREFIX=$HOME/log
isatest@13236
    16
MASTERLOG=$LOGPREFIX/isatest.log
kleing@13985
    17
ERRORLOG=$HOME/var/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@13985
    71
        MFLAGS="-j 4"
kleing@13985
    72
        ;;
kleing@13985
    73
kleing@13985
    74
    sunbroy1)
kleing@13985
    75
        MFLAGS="-j 2"
kleing@13985
    76
        ;;
isatest@13838
    77
kleing@13985
    78
    macbroy*)
kleing@13985
    79
        MFLAGS=""
kleing@13985
    80
        NICE=""
kleing@13985
    81
        ;;
isatest@13838
    82
kleing@13985
    83
    *)
kleing@13985
    84
        MFLAGS=""
kleing@13985
    85
        # be nice by default
kleing@13985
    86
        NICE=nice
isatest@13838
    87
        ;;
isatest@13838
    88
esac
isatest@13838
    89
kleing@13985
    90
# main test loop
isatest@13320
    91
kleing@13231
    92
for SETTINGS in $@; do
kleing@13231
    93
kleing@13231
    94
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
kleing@13231
    95
kleing@13231
    96
    # logfile setup
kleing@13231
    97
isatest@13432
    98
    DATE=$(date "+%Y-%m-%d")
kleing@13231
    99
    SHORT=${SETTINGS##*/}
kleing@13231
   100
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
kleing@13231
   101
kleing@13231
   102
    # the test
kleing@13231
   103
kleing@13987
   104
    touch $RUNNING/$SHORT.running
kleing@13985
   105
kleing@13231
   106
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
kleing@13231
   107
kleing@13233
   108
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
kleing@13924
   109
    $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
kleing@13231
   110
kleing@13231
   111
    if [ $? -eq 0 ]
kleing@13231
   112
    then
kleing@13985
   113
        # test log and cleanup
isatest@13236
   114
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13231
   115
        gzip -f $TESTLOG
kleing@13985
   116
        rm -rf $HOME/isabelle-$SHORT
kleing@13231
   117
    else
kleing@13985
   118
        # test log
kleing@13231
   119
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
kleing@13985
   120
kleing@13985
   121
        # error log
kleing@13985
   122
        echo "Test for platform ${SHORT}failed. Log file available at" >> $ERRORLOG
kleing@13985
   123
        echo "$HOSTNAME:$TESTLOG" >> $ERRORLOG
kleing@13985
   124
        echo "[...]" >> $ERRORLOG
kleing@13985
   125
        tail -3 $L >> $ERRORLOG
kleing@13985
   126
        echo >> $ERRORLOG
kleing@13985
   127
kleing@13985
   128
        FAIL="$FAIL$SHORT "
kleing@13231
   129
    fi
kleing@13231
   130
kleing@13987
   131
    rm -f $RUNNING/$SHORT.running
kleing@13231
   132
done
kleing@13231
   133
kleing@13985
   134
# time and success/failure to master log
isatest@13236
   135
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
isatest@13236
   136
kleing@13985
   137
if [ -z "$FAIL" ]; then
kleing@13985
   138
    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13236
   139
else
kleing@13985
   140
    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
kleing@13985
   141
    exit 1
isatest@13236
   142
fi
isatest@13236
   143
isatest@13236
   144
# end