Admin/isatest-makedist
author kleing
Sun Apr 06 21:14:02 2003 +0200 (2003-04-06)
changeset 13900 0cfdeb44621e
parent 13839 e1240620f1b5
child 13955 8ab1d3e73bb1
permissions -rwxr-xr-x
run on sunbroy1, too
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Gerwin Klein, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
     8 
     9 # source bashrc, we're called by cron
    10 . ~/.bashrc
    11 
    12 
    13 ## global settings
    14 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    15 
    16 TMP=/tmp/isatest-makedist.$$
    17 MAIL=~/bin/pmail
    18 
    19 LOGPREFIX=~/log
    20 MASTERLOG=$LOGPREFIX/isatest.log
    21 DISTPREFIX=~/isadist
    22 MAKEDIST=~/bin/makedist
    23 MAKEALL=~/bin/isatest-makeall
    24 TAR=gtar
    25 
    26 SUN=sunbroy2
    27 AT=atbroy51
    28 
    29 SSH="ssh -f"
    30 
    31 ## diagnostics
    32 
    33 PRG="$(basename "$0")"
    34 
    35 function usage()
    36 {
    37   echo
    38   echo "Usage: $PRG"
    39   echo
    40   echo "   Build distribution and run isatest-make for lots of platforms."
    41   echo
    42   exit 1
    43 }
    44 
    45 function fail()
    46 {
    47   echo "$1" >&2
    48   exit 2
    49 }
    50 
    51 ## main
    52 
    53 export DISTPREFIX
    54 
    55 DATE=$(date "+%Y-%m-%d")
    56 DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
    57 
    58 echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
    59 
    60 echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
    61 rm -rf $DISTPREFIX >> $DISTLOG 2>&1
    62 
    63 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
    64 rm -rf ~/isabelle-*
    65 
    66 echo "### building distribution"  >> $DISTLOG 2>&1
    67 $MAKEDIST - >> $DISTLOG 2>&1
    68 
    69 if [ $? -ne 0 ]
    70 then
    71     echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    72     ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    73     echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
    74 
    75     echo "Could not build isabelle distribution. Log file available at" > $TMP
    76     echo "$HOSTNAME:$DISTLOG" >> $TMP
    77 
    78     for R in $MAILTO; do
    79 	$MAIL "isabelle dist build failed" $R $TMP
    80     done
    81 
    82     rm $TMP
    83 
    84     exit 1
    85 fi
    86 
    87 cd $DISTPREFIX >> $DISTLOG 2>&1
    88 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
    89 
    90 echo "### generating development snapshot web page" >> $DISTLOG 2>&1
    91 (cd ~/devel-page; make)
    92 
    93 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    94 gzip -f $DISTLOG
    95 
    96 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    97 echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
    98 
    99 
   100 ## spawn test runs
   101 
   102 $SSH sunbroy1 "$MAKEALL $DISTPREFIX ~/settings/sun1-poly ~/settings/sun1-sml"
   103 $SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly ~/settings/sun-sml"
   104 $SSH $AT "$MAKEALL $DISTPREFIX ~/settings/at-poly ~/settings/at-sml"
   105 
   106 ## end