Admin/isatest-makeall

deleted a pointless comment

#!/usr/bin/env bash
#
# $Id$
# Author: Gerwin Klein, TU Muenchen
#
# DESCRIPTION: Run isatool makeall from specified distribution and settings.

## global settings

# canoncical home for all platforms 
HOME=/usr/stud/isatest

# where the log files are
LOGPREFIX=$HOME/log
MASTERLOG=$LOGPREFIX/isatest.log
ERRORDIR=$HOME/var
ERRORLOG=$ERRORDIR/error.log

# where to put test-is-running files
RUNNING=$HOME/var/running


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
  echo
  echo "  Runs isatool makeall from specified distribution and settings."
  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

## main

# argument checking

[ "$1" = "-?" ] && usage
[ "$#" -lt "2" ] && usage

DISTPREFIX=$1
shift

[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."

# make file flags and nice setup for different target platforms
case $HOSTNAME in
    atbroy51)
        # 2 processors
        MFLAGS="-j 2"
        # MFLAGS=""
        NICE=""
        ;;

    atbroy31)
        # cluster
        MFLAGS="-j 5"
        ;;
  
    sunbroy2)
        MFLAGS="-j 6"
	NICE="nice"
        ;;

    sunbroy1)
        MFLAGS="-j 2"
	NICE="nice"
        ;;

    macbroy*)
        MFLAGS=""
        NICE=""
        ;;

    *)
        MFLAGS=""
        # be nice by default
        NICE=nice
        ;;
esac

# main test loop

for SETTINGS in $@; do

    [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."

    # logfile setup

    DATE=$(date "+%Y-%m-%d")
    SHORT=${SETTINGS##*/}
    TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log

    # the test

    touch $RUNNING/$SHORT.running

    echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1

    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 

    if [ $? -eq 0 ]
    then
        # test log and cleanup
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
        gzip -f $TESTLOG
    else
        # test log
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1

        # error log
        echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG
        echo "[...]" >> $ERRORLOG
        tail -3 $TESTLOG >> $ERRORLOG
        echo >> $ERRORLOG

        FAIL="$FAIL$SHORT "
        (cd $ERRORDIR; ln -s $TESTLOG)
    fi

    rm -f $RUNNING/$SHORT.running
done

# time and success/failure to master log
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")

if [ -z "$FAIL" ]; then
    echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
else
    echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
    exit 1
fi

# end