Admin/isatest/isatest-makeall

removed some old/unused stuff;
tuned whitespace;

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

## global settings
. ~/admin/isatest/isatest-settings

# max time until test is aborted (in sec)
MAXTIME=28800


## diagnostics

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

function usage()
{
  echo
  echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]"
  echo
  echo "  Runs isabelle makeall for specified settings."
  echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
  echo
  echo "Examples:"
  echo "  $PRG ~/settings/at-poly ~/settings/at-sml"
  echo "  $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly"
  exit 1
}

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


## main

# argument checking

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

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

TARGETS=all

# make file flags and nice setup for different target platforms
MFLAGS="-k"
NICE="nice"
case $HOSTNAME in
    macbroy2 | macbroy6 | macbroy30)
        NICE=""
        ;;
    lxbroy[234])
        MFLAGS="-k -j 2"
        NICE=""
        ;;

esac

ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle"

[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"

if [ "$1" = "-l" ]; then
  shift
  [ "$#" -lt "3" ] && usage
  LOGIC="$1"
  TARGETS="$2"
  shift 2
  ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
  if [ "$LOGIC" = "." ]; then
    DIR="."
    TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
  else
    DIR="$ISABELLE_HOME/src/$LOGIC"
    TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
  fi
else
  DIR="."
  TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
fi

IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT")


# main test loop

log "starting [$@]"

for SETTINGS in $@; do

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

    # logfile setup

    DATE=$(date "+%Y-%m-%d")
    SHORT=${SETTINGS##*/}

    if [ "${SHORT%-e}" == "$SHORT" ]; then
        # normal test
        TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
    else
        # experimental test
        TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log
    fi

    # the test

    touch $RUNNING/$SHORT.running

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

    echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1

    if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then
        echo "--- cleaning up old $ISABELLE_HOME_USER"
        rm -rf $ISABELLE_HOME_USER
    fi

    cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings
    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    (ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $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; cp $TESTLOG .)
    fi

    rm -f $RUNNING/$SHORT.running
done

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

if [ -z "$FAIL" ]; then
    log "all tests successful, elapsed time $ELAPSED."
else
    log "targets ${FAIL}FAILED, elapsed time $ELAPSED."
    exit 1
fi