Admin/isatest-makedist
changeset 13231 cce28efb2600
child 13233 5ab7bac534c9
equal deleted inserted replaced
13230:c5fad3c40d45 13231:cce28efb2600
       
     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 ## global settings
       
    10 LOGPREFIX=~
       
    11 DISTPREFIX=~/isadist
       
    12 MAKEDIST=~/bin/makedist
       
    13 
       
    14 SUN=sunbroy2
       
    15 AT=atbroy37
       
    16 
       
    17 SSH="ssh -1 -f"
       
    18 
       
    19 ## diagnostics
       
    20 
       
    21 PRG="$(basename "$0")"
       
    22 
       
    23 function usage()
       
    24 {
       
    25   echo
       
    26   echo "Usage: $PRG"
       
    27   echo
       
    28   echo "   Build distribution and run isatest-make for lots of platforms."
       
    29   echo
       
    30   exit 1
       
    31 }
       
    32 
       
    33 function fail()
       
    34 {
       
    35   echo "$1" >&2
       
    36   exit 2
       
    37 }
       
    38 
       
    39 ## main
       
    40 
       
    41 export DISTPREFIX
       
    42 
       
    43 DATE=$(date "+%d-%b-%Y")
       
    44 DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
       
    45 
       
    46 # get newest version of makedist:
       
    47 # cvs -d sunbroy2:/usr/proj/isabelle-repository/archive co isabelle/Admin > $COUTLOG
       
    48 
       
    49 echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
       
    50 
       
    51 echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
       
    52 rm -rf $DISTPREFIX >> $DISTLOG 2>&1
       
    53 
       
    54 echo "### building distribution"  >> $DISTLOG 2>&1
       
    55 $MAKEDIST - >> $DISTLOG 2>&1
       
    56 
       
    57 if [ $? -ne 0 ]
       
    58 then
       
    59     echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
       
    60     # more action here
       
    61     exit 1
       
    62 fi
       
    63 
       
    64 cd $DISTPREFIX >> $DISTLOG 2>&1
       
    65 tar xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
       
    66 
       
    67 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
       
    68 
       
    69 ## spawn test runs
       
    70 
       
    71 # run tests in parallel on multiprocessor sun 
       
    72 $SSH $SUN sun-poly   
       
    73 $SSH $SUN sun-sml
       
    74 
       
    75 # run tests sequentially on x86
       
    76 $SSH $AT at-poly at-sml
       
    77 
       
    78 ## end