Admin/isatest-makeall
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 14280 d7c3691008f9
child 14433 f25291a96e17
permissions -rwxr-xr-x
generic of_nat and of_int functions, and generalization of iszero and neg
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     1
#!/usr/bin/env bash
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     2
#
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     3
# $Id$
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     4
# Author: Gerwin Klein, TU Muenchen
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     6
#
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     7
# DESCRIPTION: Run isatool makeall from specified distribution and settings.
13962
908f6776a59b use /usr/stud/isatest as home for all platforms (macbroy33 has no /home/stud/..)
kleing
parents: 13924
diff changeset
     8
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     9
## global settings
13246
e51efc2029e9 email sending
isatest
parents: 13236
diff changeset
    10
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    11
# canoncical home for all platforms 
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    12
HOME=/usr/stud/isatest
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    13
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    14
# where the log files are
13962
908f6776a59b use /usr/stud/isatest as home for all platforms (macbroy33 has no /home/stud/..)
kleing
parents: 13924
diff changeset
    15
LOGPREFIX=$HOME/log
13236
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
    16
MASTERLOG=$LOGPREFIX/isatest.log
14035
c46ce87960fb attach log files
kleing
parents: 14012
diff changeset
    17
ERRORDIR=$HOME/var
c46ce87960fb attach log files
kleing
parents: 14012
diff changeset
    18
ERRORLOG=$ERRORDIR/error.log
13236
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
    19
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    20
# where to put test-is-running files
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    21
RUNNING=$HOME/var/running
13320
2c6ee189ae63 send email plaform independently
isatest
parents: 13246
diff changeset
    22
2c6ee189ae63 send email plaform independently
isatest
parents: 13246
diff changeset
    23
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    24
## diagnostics
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    25
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    26
PRG="$(basename "$0")"
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    27
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    28
function usage()
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    29
{
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    30
  echo
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    31
  echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    32
  echo
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    33
  echo "  Runs isatool makeall from specified distribution and settings."
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    34
  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    35
  echo
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    36
  exit 1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    37
}
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    38
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    39
function fail()
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    40
{
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    41
  echo "$1" >&2
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    42
  exit 2
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    43
}
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    44
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    45
## main
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    46
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    47
# argument checking
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    48
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    49
[ "$1" = "-?" ] && usage
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    50
[ "$#" -lt "2" ] && usage
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    51
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    52
DISTPREFIX=$1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    53
shift
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    54
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    55
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    56
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    57
# make file flags and nice setup for different target platforms
13838
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    58
case $HOSTNAME in
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    59
    atbroy51)
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    60
        # 2 processors
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    61
        MFLAGS="-j 2"
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    62
        # MFLAGS=""
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    63
        NICE=""
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    64
        ;;
13838
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    65
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    66
    atbroy31)
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    67
        # cluster
13838
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    68
        MFLAGS="-j 5"
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    69
        ;;
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    70
  
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    71
    sunbroy2)
13990
kleing
parents: 13987
diff changeset
    72
        MFLAGS="-j 6"
14012
9d1f027eb4e8 be nice on sunbroy2
kleing
parents: 13994
diff changeset
    73
	NICE="nice"
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    74
        ;;
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    75
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    76
    sunbroy1)
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    77
        MFLAGS="-j 2"
14012
9d1f027eb4e8 be nice on sunbroy2
kleing
parents: 13994
diff changeset
    78
	NICE="nice"
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    79
        ;;
13838
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    80
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    81
    macbroy*)
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    82
        MFLAGS=""
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    83
        NICE=""
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    84
        ;;
13838
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    85
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    86
    *)
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    87
        MFLAGS=""
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    88
        # be nice by default
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    89
        NICE=nice
13838
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    90
        ;;
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    91
esac
fe83f2231767 case distinction on host for makefile flags
isatest
parents: 13432
diff changeset
    92
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
    93
# main test loop
13320
2c6ee189ae63 send email plaform independently
isatest
parents: 13246
diff changeset
    94
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    95
for SETTINGS in $@; do
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    96
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    97
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    98
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    99
    # logfile setup
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   100
13432
470daa444967 - changed date format for proper lexicographical ordering
isatest
parents: 13359
diff changeset
   101
    DATE=$(date "+%Y-%m-%d")
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   102
    SHORT=${SETTINGS##*/}
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   103
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   104
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   105
    # the test
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   106
13987
kleing
parents: 13985
diff changeset
   107
    touch $RUNNING/$SHORT.running
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   108
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   109
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   110
13233
kleing
parents: 13232
diff changeset
   111
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
13924
09f6f2fefb25 no need to be nice everywhere
kleing
parents: 13901
diff changeset
   112
    $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   113
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   114
    if [ $? -eq 0 ]
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   115
    then
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   116
        # test log and cleanup
13236
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
   117
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   118
        gzip -f $TESTLOG
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   119
        rm -rf $HOME/isabelle-$SHORT
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   120
    else
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   121
        # test log
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   122
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   123
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   124
        # error log
14035
c46ce87960fb attach log files
kleing
parents: 14012
diff changeset
   125
        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   126
        echo "[...]" >> $ERRORLOG
14035
c46ce87960fb attach log files
kleing
parents: 14012
diff changeset
   127
        tail -3 $TESTLOG >> $ERRORLOG
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   128
        echo >> $ERRORLOG
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   129
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   130
        FAIL="$FAIL$SHORT "
14035
c46ce87960fb attach log files
kleing
parents: 14012
diff changeset
   131
        (cd $ERRORDIR; ln -s $TESTLOG)
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   132
    fi
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   133
13987
kleing
parents: 13985
diff changeset
   134
    rm -f $RUNNING/$SHORT.running
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   135
done
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   136
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   137
# time and success/failure to master log
13236
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
   138
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
   139
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   140
if [ -z "$FAIL" ]; then
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   141
    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
13236
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
   142
else
13985
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   143
    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
3852929a8d1d leave error messages in error.log, send only one email for all platforms
kleing
parents: 13962
diff changeset
   144
    exit 1
13236
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
   145
fi
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
   146
568bc754d303 included masterlog file
isatest
parents: 13233
diff changeset
   147
# end