Admin/isatest-makeall
changeset 13985 3852929a8d1d
parent 13962 908f6776a59b
child 13987 31891dd8c04b
equal deleted inserted replaced
13984:e055ba9020eb 13985:3852929a8d1d
     3 # $Id$
     3 # $Id$
     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: Run isatool makeall from specified distribution and settings.
     7 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
     8 #              Send email if it fails.
       
     9 
     8 
    10 # canoncical home for all platforms
     9 ## global settings
       
    10 
       
    11 # canoncical home for all platforms 
    11 HOME=/usr/stud/isatest
    12 HOME=/usr/stud/isatest
    12 
    13 
    13 ## global settings
    14 # where the log files are
    14 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
    15 LOGPREFIX=$HOME/log
       
    16 MASTERLOG=$LOGPREFIX/isatest.log
       
    17 ERRORLOG=$HOME/var/error.log
    15 
    18 
    16 LOGPREFIX=$HOME/log
    19 # where to put test-is-running files
       
    20 RUNNING=$HOME/var/running
    17 
    21 
    18 MASTERLOG=$LOGPREFIX/isatest.log
       
    19 
       
    20 TMP=/tmp/isatest-makeall.$$
       
    21 
       
    22 MAIL=$HOME/bin/pmail
       
    23 
    22 
    24 ## diagnostics
    23 ## diagnostics
    25 
    24 
    26 PRG="$(basename "$0")"
    25 PRG="$(basename "$0")"
    27 
    26 
    28 function usage()
    27 function usage()
    29 {
    28 {
    30   echo
    29   echo
    31   echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
    30   echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
    32   echo
    31   echo
    33   echo "  Run isatool makeall from specified distribution and settings."
    32   echo "  Runs isatool makeall from specified distribution and settings."
    34   echo "  Send email if it fails."
    33   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
    35   echo
    34   echo
    36   exit 1
    35   exit 1
    37 }
    36 }
    38 
    37 
    39 function fail()
    38 function fail()
    52 DISTPREFIX=$1
    51 DISTPREFIX=$1
    53 shift
    52 shift
    54 
    53 
    55 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    54 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    56 
    55 
    57 NICE=nice
    56 # make file flags and nice setup for different target platforms
       
    57 case $HOSTNAME in
       
    58     atbroy51)
       
    59         # 2 processors
       
    60         MFLAGS="-j 2"
       
    61         # MFLAGS=""
       
    62         NICE=""
       
    63         ;;
    58 
    64 
    59 case $HOSTNAME in
    65     atbroy31)
    60         atbroy51)
    66         # cluster
    61 	MFLAGS="-j 2"
       
    62 	# MFLAGS=""
       
    63   NICE=""
       
    64 	;;
       
    65 
       
    66         atbroy31)
       
    67         MFLAGS="-j 5"
    67         MFLAGS="-j 5"
    68         ;;
    68         ;;
    69 	
    69   
    70 	atbroy12)
    70     sunbroy2)
    71 	MFLAGS="-j 5"
    71         MFLAGS="-j 4"
    72 	;;
    72         ;;
    73 
    73 
    74 	sunbroy2)
    74     sunbroy1)
    75 	MFLAGS="-j 4"
    75         MFLAGS="-j 2"
    76 	;;
    76         ;;
    77 
    77 
    78 	sunbroy1)
    78     macbroy*)
    79 	MFLAGS="-j 2"
    79         MFLAGS=""
    80 	;;
    80         NICE=""
       
    81         ;;
    81 
    82 
    82    	*)
    83     *)
    83 	MFLAGS=""
    84         MFLAGS=""
       
    85         # be nice by default
       
    86         NICE=nice
    84         ;;
    87         ;;
    85 esac
    88 esac
    86 
    89 
    87 
    90 # main test loop
    88 
       
    89 LOGS=""
       
    90 
    91 
    91 for SETTINGS in $@; do
    92 for SETTINGS in $@; do
    92 
    93 
    93     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    94     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    94     
       
    95 
    95 
    96     # logfile setup
    96     # logfile setup
    97 
    97 
    98     DATE=$(date "+%Y-%m-%d")
    98     DATE=$(date "+%Y-%m-%d")
    99     SHORT=${SETTINGS##*/}
    99     SHORT=${SETTINGS##*/}
   100     TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
   100     TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
   101 
   101 
   102     # the test
   102     # the test
   103 
   103 
       
   104     touch $RUNNING/$SHORT
       
   105 
   104     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   106     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   105 
   107 
   106     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   108     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   107     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   109     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   108 
   110 
   109     if [ $? -eq 0 ]
   111     if [ $? -eq 0 ]
   110     then
   112     then
       
   113         # test log and cleanup
   111         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   114         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   112         gzip -f $TESTLOG
   115         gzip -f $TESTLOG
   113 	rm -rf $HOME/isabelle-$SHORT
   116         rm -rf $HOME/isabelle-$SHORT
   114     else
   117     else
       
   118         # test log
   115         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   119         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   116 	FAIL="$FAIL$SHORT "
   120 
   117 	LOGS="${LOGS}$TESTLOG "
   121         # error log
       
   122         echo "Test for platform ${SHORT}failed. Log file available at" >> $ERRORLOG
       
   123         echo "$HOSTNAME:$TESTLOG" >> $ERRORLOG
       
   124         echo "[...]" >> $ERRORLOG
       
   125         tail -3 $L >> $ERRORLOG
       
   126         echo >> $ERRORLOG
       
   127 
       
   128         FAIL="$FAIL$SHORT "
   118     fi
   129     fi
   119 
   130 
       
   131     rm -f $RUNNING/$SHORT
   120 done
   132 done
   121 
   133 
       
   134 # time and success/failure to master log
   122 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   135 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   123 
   136 
   124 if [ "$FAIL" != "" ]; then
   137 if [ -z "$FAIL" ]; then
   125 	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
   138     echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
   126 	
       
   127 	echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP
       
   128 	for L in $LOGS; do 
       
   129 		echo "$HOSTNAME:$L" >> $TMP 
       
   130 		echo "[...]" >> $TMP
       
   131 		tail -3 $L >> $TMP
       
   132 		echo >> $TMP
       
   133 	done
       
   134 	echo "Have a nice day," >> $TMP
       
   135 	echo "  isatest" >> $TMP
       
   136 
       
   137         for R in $MAILTO; do
       
   138 	    $MAIL "isabelle test failed" $R $TMP
       
   139 	done
       
   140 
       
   141 	rm $TMP
       
   142 
       
   143 	exit 1
       
   144 else
   139 else
   145         echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
   140     echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
       
   141     exit 1
   146 fi
   142 fi
   147 
   143 
   148 # end
   144 # end