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