Admin/isatest-makeall
author mehta
Fri Apr 16 15:46:50 2004 +0200 (2004-04-16)
changeset 14591 7be4d5dadf15
parent 14433 f25291a96e17
child 14981 e73f8140af78
permissions -rwxr-xr-x
lemma drop_Suc_conv_tl added.
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 # Author: Gerwin Klein, TU Muenchen
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     6 #
     7 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
     8 
     9 ## global settings
    10 
    11 # canoncical home for all platforms 
    12 HOME=/usr/stud/isatest
    13 
    14 # where the log files are
    15 LOGPREFIX=$HOME/log
    16 MASTERLOG=$LOGPREFIX/isatest.log
    17 ERRORDIR=$HOME/var
    18 ERRORLOG=$ERRORDIR/error.log
    19 
    20 # where to put test-is-running files
    21 RUNNING=$HOME/var/running
    22 
    23 
    24 ## diagnostics
    25 
    26 PRG="$(basename "$0")"
    27 
    28 function usage()
    29 {
    30   echo
    31   echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
    32   echo
    33   echo "  Runs isatool makeall from specified distribution and settings."
    34   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
    35   echo
    36   exit 1
    37 }
    38 
    39 function fail()
    40 {
    41   echo "$1" >&2
    42   exit 2
    43 }
    44 
    45 ## main
    46 
    47 # argument checking
    48 
    49 [ "$1" = "-?" ] && usage
    50 [ "$#" -lt "2" ] && usage
    51 
    52 DISTPREFIX=$1
    53 shift
    54 
    55 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
    56 
    57 # make file flags and nice setup for different target platforms
    58 case $HOSTNAME in
    59     atbroy51)
    60         # 2 processors
    61         MFLAGS="-j 2"
    62         # MFLAGS=""
    63         NICE=""
    64         ;;
    65 
    66     atbroy31)
    67         # cluster
    68         MFLAGS="-j 5"
    69         ;;
    70   
    71     sunbroy2)
    72         MFLAGS="-j 6"
    73 	NICE="nice"
    74         ;;
    75 
    76     sunbroy1)
    77         MFLAGS="-j 2"
    78 	NICE="nice"
    79         ;;
    80 
    81     macbroy*)
    82         MFLAGS=""
    83         NICE=""
    84         ;;
    85 
    86     *)
    87         MFLAGS=""
    88         # be nice by default
    89         NICE=nice
    90         ;;
    91 esac
    92 
    93 # main test loop
    94 
    95 for SETTINGS in $@; do
    96 
    97     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
    98 
    99     # logfile setup
   100 
   101     DATE=$(date "+%Y-%m-%d")
   102     SHORT=${SETTINGS##*/}
   103     TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
   104 
   105     # the test
   106 
   107     touch $RUNNING/$SHORT.running
   108 
   109     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
   110 
   111     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
   112     $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 
   113 
   114     if [ $? -eq 0 ]
   115     then
   116         # test log and cleanup
   117         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   118         gzip -f $TESTLOG
   119     else
   120         # test log
   121         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
   122 
   123         # error log
   124         echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
   125         echo "[...]" >> $ERRORLOG
   126         tail -3 $TESTLOG >> $ERRORLOG
   127         echo >> $ERRORLOG
   128 
   129         FAIL="$FAIL$SHORT "
   130         (cd $ERRORDIR; ln -s $TESTLOG)
   131     fi
   132 
   133     rm -f $RUNNING/$SHORT.running
   134 done
   135 
   136 # time and success/failure to master log
   137 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   138 
   139 if [ -z "$FAIL" ]; then
   140     echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
   141 else
   142     echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
   143     exit 1
   144 fi
   145 
   146 # end