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