Admin/isatest-makedist
changeset 13237 493d61afa731
parent 13234 8139edae3bf5
child 13246 e51efc2029e9
equal deleted inserted replaced
13236:568bc754d303 13237:493d61afa731
     4 # Author: Gerwin Klein, TU Muenchen
     4 # Author: Gerwin Klein, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     6 #
     7 # DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
     7 # DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
     8 
     8 
       
     9 # source bashrc, we're called by cron
       
    10 . ~/.bashrc
       
    11 
       
    12 
     9 ## global settings
    13 ## global settings
    10 LOGPREFIX=~/log
    14 LOGPREFIX=~/log
       
    15 MASTERLOG=$LOGPREFIX/isatest.log
    11 DISTPREFIX=~/isadist
    16 DISTPREFIX=~/isadist
    12 MAKEDIST=~/bin/makedist
    17 MAKEDIST=~/bin/makedist
    13 MAKEALL=~/bin/isatest-makeall
    18 MAKEALL=~/bin/isatest-makeall
    14 TAR=gtar
    19 TAR=gtar
    15 
    20 
    48 echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
    53 echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
    49 
    54 
    50 echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
    55 echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
    51 rm -rf $DISTPREFIX >> $DISTLOG 2>&1
    56 rm -rf $DISTPREFIX >> $DISTLOG 2>&1
    52 
    57 
       
    58 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
       
    59 rm -rf ~/isabelle-*
       
    60 
    53 echo "### building distribution"  >> $DISTLOG 2>&1
    61 echo "### building distribution"  >> $DISTLOG 2>&1
    54 $MAKEDIST - >> $DISTLOG 2>&1
    62 $MAKEDIST - >> $DISTLOG 2>&1
    55 
    63 
    56 if [ $? -ne 0 ]
    64 if [ $? -ne 0 ]
    57 then
    65 then
    58     echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    66     echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
       
    67     ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
       
    68     echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
    59     # more action here
    69     # more action here
    60     exit 1
    70     exit 1
    61 fi
    71 fi
    62 
    72 
    63 cd $DISTPREFIX >> $DISTLOG 2>&1
    73 cd $DISTPREFIX >> $DISTLOG 2>&1
    64 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
    74 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
    65 
    75 
    66 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    76 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
       
    77 gzip -f $DISTLOG
       
    78 
       
    79 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
       
    80 echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
       
    81 
    67 
    82 
    68 ## spawn test runs
    83 ## spawn test runs
    69 
    84 
    70 # run tests in parallel on multiprocessor sun 
    85 # run tests in parallel on multiprocessor sun 
    71 $SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly"
    86 $SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly"