Admin/isatest-makeall
changeset 13320 2c6ee189ae63
parent 13246 e51efc2029e9
child 13359 982827aacb39
equal deleted inserted replaced
13319:23de7b3af453 13320:2c6ee189ae63
    11 MAILTO="kleing@in.tum.de test@jflex.de"
    11 MAILTO="kleing@in.tum.de test@jflex.de"
    12 
    12 
    13 LOGPREFIX=~/log
    13 LOGPREFIX=~/log
    14 
    14 
    15 MASTERLOG=$LOGPREFIX/isatest.log
    15 MASTERLOG=$LOGPREFIX/isatest.log
       
    16 
       
    17 TMP=/tmp/isatest-makeall.$$
       
    18 
       
    19 MAIL=~/bin/pmail
    16 
    20 
    17 ## diagnostics
    21 ## diagnostics
    18 
    22 
    19 PRG="$(basename "$0")"
    23 PRG="$(basename "$0")"
    20 
    24 
    45 DISTPREFIX=$1
    49 DISTPREFIX=$1
    46 shift
    50 shift
    47 
    51 
    48 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    52 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    49 
    53 
       
    54 LOGS=""
       
    55 
    50 for SETTINGS in $@; do
    56 for SETTINGS in $@; do
    51 
    57 
    52     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    58     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    53     
    59     
    54 
    60 
    60 
    66 
    61     # the test
    67     # the test
    62 
    68 
    63     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
    69     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
    64 
    70 
    65     cp $DISTPREFIX/Isabelle/etc/settings $DISTPREFIX/Isabelle/etc/settings.save-$SHORT
       
    66     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    71     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    67     $DISTPREFIX/Isabelle/bin/isatool makeall all >> $TESTLOG 2>&1 
    72     nice $DISTPREFIX/Isabelle/bin/isatool makeall -j 2 all >> $TESTLOG 2>&1 
    68 
    73 
    69     if [ $? -eq 0 ]
    74     if [ $? -eq 0 ]
    70     then
    75     then
    71         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    76         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    72         mv $DISTPREFIX/Isabelle/etc/settings.save-$SHORT $DISTPREFIX/Isabelle/etc/settings
       
    73         gzip -f $TESTLOG
    77         gzip -f $TESTLOG
    74 	rm -rf ~/isabelle-$SHORT
    78 	rm -rf ~/isabelle-$SHORT
    75     else
    79     else
    76         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    80         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
    77 	FAIL="$FAIL$SHORT "
    81 	FAIL="$FAIL$SHORT "
    78 	for R in $MAILTO; do
    82 	LOGS="${LOGS}$HOSTNAME:$TESTLOG\n"
    79     		mail -t $R <<EOM
       
    80 Subject: isabelle test failed
       
    81 
       
    82 Test for platform $SHORT failed. Log file available at
       
    83 
       
    84 $HOSTNAME:$TESTLOG
       
    85 EOM
       
    86 	done
       
    87         # more action here
       
    88     fi
    83     fi
    89 
    84 
    90 done
    85 done
    91 
    86 
    92 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    87 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    93 
    88 
    94 if [ "$FAIL" != "" ]; then
    89 if [ "$FAIL" != "" ]; then
    95 	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
    90 	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
       
    91 	
       
    92 	echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP
       
    93 	echo "$LOGS" >> $TMP
       
    94 
       
    95         for R in $MAILTO; do
       
    96 	    $MAIL "isabelle test failed" $R $TMP
       
    97 	done
       
    98 
       
    99 	rm $TMP
       
   100 
    96 	exit 1
   101 	exit 1
    97 else
   102 else
    98         echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
   103         echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
    99 fi
   104 fi
   100 
   105