Admin/isatest/isatest-makeall
changeset 22410 da313b67a04d
child 22411 1956d895a4ed
equal deleted inserted replaced
22409:5f7c9c82b05e 22410:da313b67a04d
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # $Id$
       
     4 # Author: Gerwin Klein, TU Muenchen
       
     5 #
       
     6 # DESCRIPTION: Run isatool makeall from specified distribution and settings.
       
     7 
       
     8 ## global settings
       
     9 . ~/admin/isatest-settings
       
    10 
       
    11 # max time until test is aborted (in sec)
       
    12 MAXTIME=28800
       
    13 
       
    14 ## diagnostics
       
    15 
       
    16 PRG="$(basename "$0")"
       
    17 
       
    18 function usage()
       
    19 {
       
    20   echo
       
    21   echo "Usage: $PRG settings1 [settings2 ...]"
       
    22   echo
       
    23   echo "  Runs isatool makeall for specified settings."
       
    24   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
       
    25   echo
       
    26   exit 1
       
    27 }
       
    28 
       
    29 function fail()
       
    30 {
       
    31   echo "$1" >&2
       
    32   echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
       
    33   exit 2
       
    34 }
       
    35 
       
    36 ## main
       
    37 
       
    38 # argument checking
       
    39 
       
    40 [ "$1" = "-?" ] && usage
       
    41 [ "$#" -lt "1" ] && usage
       
    42 
       
    43 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
       
    44 
       
    45 # make file flags and nice setup for different target platforms
       
    46 case $HOSTNAME in
       
    47     atbroy51)
       
    48         # 2 processors
       
    49         MFLAGS="-j 2"
       
    50         # MFLAGS=""
       
    51         NICE=""
       
    52         ;;
       
    53 
       
    54     atbroy31)
       
    55         # cluster
       
    56         MFLAGS="-j 5"
       
    57         ;;
       
    58   
       
    59     sunbroy2)
       
    60         MFLAGS="-j 6"
       
    61         NICE="nice"
       
    62         ;;
       
    63 
       
    64     sunbroy1)
       
    65         MFLAGS="-j 2"
       
    66         NICE="nice"
       
    67         ;;
       
    68 
       
    69     macbroy5)
       
    70         MFLAGS="" # -j 2 does not work on poly/macos 10.4.1
       
    71         NICE=""
       
    72         ;;
       
    73 
       
    74     *)
       
    75         MFLAGS=""
       
    76         # be nice by default
       
    77         NICE=nice
       
    78         ;;
       
    79 esac
       
    80 
       
    81 # main test loop
       
    82 
       
    83 for SETTINGS in $@; do
       
    84 
       
    85     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
       
    86 
       
    87     # logfile setup
       
    88 
       
    89     DATE=$(date "+%Y-%m-%d")
       
    90     SHORT=${SETTINGS##*/}
       
    91     TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
       
    92 
       
    93     # the test
       
    94 
       
    95     touch $RUNNING/$SHORT.running
       
    96 
       
    97     echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
       
    98 
       
    99     cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
       
   100     (ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1)
       
   101 
       
   102     if [ $? -eq 0 ]
       
   103     then
       
   104         # test log and cleanup
       
   105         echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
       
   106         gzip -f $TESTLOG
       
   107     else
       
   108         # test log
       
   109         echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
       
   110 
       
   111         # error log
       
   112         echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
       
   113         echo "[...]" >> $ERRORLOG
       
   114         tail -3 $TESTLOG >> $ERRORLOG
       
   115         echo >> $ERRORLOG
       
   116 
       
   117         FAIL="$FAIL$SHORT "
       
   118         (cd $ERRORDIR; ln -s $TESTLOG)
       
   119     fi
       
   120 
       
   121     rm -f $RUNNING/$SHORT.running
       
   122 done
       
   123 
       
   124 # time and success/failure to master log
       
   125 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
       
   126 
       
   127 if [ -z "$FAIL" ]; then
       
   128     echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
       
   129 else
       
   130     echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
       
   131     exit 1
       
   132 fi
       
   133 
       
   134 # end