Admin/isatest/isatest-makeall
author urbanc
Thu, 13 Sep 2007 23:58:38 +0200
changeset 24571 a6d0428dea8e
parent 23415 9dad8095bd43
child 24647 212c9b342a67
permissions -rwxr-xr-x
some cleaning up to do with contexts
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     1
#!/usr/bin/env bash
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     2
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     3
# $Id$
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     4
# Author: Gerwin Klein, TU Muenchen
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     5
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     6
# DESCRIPTION: Run isatool makeall from specified distribution and settings.
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     7
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
     8
## global settings
22411
1956d895a4ed adjust paths
kleing
parents: 22410
diff changeset
     9
. ~/admin/isatest/isatest-settings
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    10
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    11
# max time until test is aborted (in sec)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    12
MAXTIME=28800
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    13
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    14
## diagnostics
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    15
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    16
PRG="$(basename "$0")"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    17
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    18
function usage()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    19
{
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    20
  echo
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    21
  echo "Usage: $PRG settings1 [settings2 ...]"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    22
  echo
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    23
  echo "  Runs isatool makeall for specified settings."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    24
  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    25
  echo
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    26
  exit 1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    27
}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    28
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    29
function fail()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    30
{
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    31
  echo "$1" >&2
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    32
  echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    33
  exit 2
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    34
}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    35
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    36
## main
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    37
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    38
# argument checking
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    39
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    40
[ "$1" = "-?" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    41
[ "$#" -lt "1" ] && usage
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    42
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    43
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    44
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    45
# make file flags and nice setup for different target platforms
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    46
case $HOSTNAME in
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    47
    atbroy51)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    48
        # 2 processors
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    49
        MFLAGS="-j 2"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    50
        # MFLAGS=""
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    51
        NICE=""
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    52
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    53
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    54
    atbroy31)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    55
        # cluster
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    56
        MFLAGS="-j 5"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    57
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    58
  
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    59
    sunbroy2)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    60
        MFLAGS="-j 6"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    61
        NICE="nice"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    62
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    63
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    64
    sunbroy1)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    65
        MFLAGS="-j 2"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    66
        NICE="nice"
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    67
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    68
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    69
    macbroy5)
23415
9dad8095bd43 macbroy5: trying -j 2;
wenzelm
parents: 22411
diff changeset
    70
        MFLAGS="-j 2"
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    71
        NICE=""
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    72
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    73
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    74
    *)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    75
        MFLAGS=""
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    76
        # be nice by default
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    77
        NICE=nice
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    78
        ;;
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    79
esac
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    80
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    81
# main test loop
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    82
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    83
for SETTINGS in $@; do
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    84
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    85
    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    86
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    87
    # logfile setup
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    88
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    89
    DATE=$(date "+%Y-%m-%d")
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    90
    SHORT=${SETTINGS##*/}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    91
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    92
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    93
    # the test
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    94
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    95
    touch $RUNNING/$SHORT.running
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    96
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    97
    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    98
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    99
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   100
    (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   101
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   102
    if [ $? -eq 0 ]
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   103
    then
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   104
        # test log and cleanup
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   105
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   106
        gzip -f $TESTLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   107
    else
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   108
        # test log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   109
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   110
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   111
        # error log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   112
        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   113
        echo "[...]" >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   114
        tail -3 $TESTLOG >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   115
        echo >> $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   116
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   117
        FAIL="$FAIL$SHORT "
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   118
        (cd $ERRORDIR; ln -s $TESTLOG)
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   119
    fi
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   120
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   121
    rm -f $RUNNING/$SHORT.running
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   122
done
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   123
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   124
# time and success/failure to master log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   125
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   126
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   127
if [ -z "$FAIL" ]; then
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   128
    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   129
else
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   130
    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   131
    exit 1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   132
fi
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   133
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   134
# end