Admin/isatest-makedist
author isatest
Sat Oct 26 13:05:27 2002 +0200 (2002-10-26)
changeset 13680 a6ce43a59d4a
parent 13431 b0ba3b3573e1
child 13839 e1240620f1b5
permissions -rwxr-xr-x
switched to atbroy51, removed markus from email list
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: Build distribution and run isatest-make for lots of platforms.
kleing@13231
     8
isatest@13237
     9
# source bashrc, we're called by cron
isatest@13237
    10
. ~/.bashrc
isatest@13237
    11
isatest@13237
    12
kleing@13231
    13
## global settings
isatest@13680
    14
MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
isatest@13359
    15
isatest@13359
    16
TMP=/tmp/isatest-makedist.$$
isatest@13359
    17
MAIL=~/bin/pmail
isatest@13246
    18
kleing@13233
    19
LOGPREFIX=~/log
isatest@13237
    20
MASTERLOG=$LOGPREFIX/isatest.log
kleing@13231
    21
DISTPREFIX=~/isadist
kleing@13231
    22
MAKEDIST=~/bin/makedist
isatest@13234
    23
MAKEALL=~/bin/isatest-makeall
isatest@13234
    24
TAR=gtar
kleing@13231
    25
kleing@13231
    26
SUN=sunbroy2
isatest@13680
    27
AT=atbroy51
kleing@13231
    28
kleing@13233
    29
SSH="ssh -f"
kleing@13231
    30
kleing@13231
    31
## diagnostics
kleing@13231
    32
kleing@13231
    33
PRG="$(basename "$0")"
kleing@13231
    34
kleing@13231
    35
function usage()
kleing@13231
    36
{
kleing@13231
    37
  echo
kleing@13231
    38
  echo "Usage: $PRG"
kleing@13231
    39
  echo
kleing@13231
    40
  echo "   Build distribution and run isatest-make for lots of platforms."
kleing@13231
    41
  echo
kleing@13231
    42
  exit 1
kleing@13231
    43
}
kleing@13231
    44
kleing@13231
    45
function fail()
kleing@13231
    46
{
kleing@13231
    47
  echo "$1" >&2
kleing@13231
    48
  exit 2
kleing@13231
    49
}
kleing@13231
    50
kleing@13231
    51
## main
kleing@13231
    52
kleing@13231
    53
export DISTPREFIX
kleing@13231
    54
isatest@13431
    55
DATE=$(date "+%Y-%m-%d")
kleing@13231
    56
DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
kleing@13231
    57
kleing@13231
    58
echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
kleing@13231
    59
kleing@13231
    60
echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
kleing@13231
    61
rm -rf $DISTPREFIX >> $DISTLOG 2>&1
kleing@13231
    62
isatest@13237
    63
echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
isatest@13237
    64
rm -rf ~/isabelle-*
isatest@13237
    65
kleing@13231
    66
echo "### building distribution"  >> $DISTLOG 2>&1
kleing@13231
    67
$MAKEDIST - >> $DISTLOG 2>&1
kleing@13231
    68
kleing@13231
    69
if [ $? -ne 0 ]
kleing@13231
    70
then
kleing@13231
    71
    echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
isatest@13237
    72
    ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
isatest@13237
    73
    echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13246
    74
isatest@13359
    75
    echo "Could not build isabelle distribution. Log file available at" > $TMP
isatest@13359
    76
    echo "$HOSTNAME:$DISTLOG" >> $TMP
isatest@13246
    77
isatest@13359
    78
    for R in $MAILTO; do
isatest@13359
    79
	$MAIL "isabelle dist build failed" $R $TMP
isatest@13246
    80
    done
isatest@13246
    81
isatest@13359
    82
    rm $TMP
isatest@13359
    83
kleing@13231
    84
    exit 1
kleing@13231
    85
fi
kleing@13231
    86
kleing@13231
    87
cd $DISTPREFIX >> $DISTLOG 2>&1
isatest@13234
    88
$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
kleing@13231
    89
kleing@13231
    90
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
isatest@13237
    91
gzip -f $DISTLOG
isatest@13237
    92
isatest@13237
    93
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
isatest@13237
    94
echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
isatest@13237
    95
kleing@13231
    96
kleing@13231
    97
## spawn test runs
kleing@13231
    98
kleing@13231
    99
# run tests in parallel on multiprocessor sun 
isatest@13246
   100
$SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly ~/settings/sun-sml"
kleing@13231
   101
kleing@13231
   102
# run tests sequentially on x86
isatest@13234
   103
$SSH $AT "$MAKEALL $DISTPREFIX ~/settings/at-poly ~/settings/at-sml"
kleing@13231
   104
isatest@13234
   105
## end