Admin/isatest-makeall

fixed "latex capacity exceeded"

#!/usr/bin/env bash
#
# $Id$
# Author: Gerwin Klein, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: Run isatool makeall from specified distribution and settings.
#              Send email if it fails.

## global settings
MAILTO="[e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail]"

LOGPREFIX=~/log

MASTERLOG=$LOGPREFIX/isatest.log

TMP=/tmp/isatest-makeall.$$

MAIL=~/bin/pmail

## diagnostics

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

function usage()
{
  echo
  echo "Usage: $PRG distributionpath settings1 [settings2 ...]"
  echo
  echo "  Run isatool makeall from specified distribution and settings."
  echo "  Send email 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."

LOGS=""

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

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

    cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings
    nice $DISTPREFIX/Isabelle/bin/isatool makeall -j 2 all >> $TESTLOG 2>&1 

    if [ $? -eq 0 ]
    then
        echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
        gzip -f $TESTLOG
	rm -rf ~/isabelle-$SHORT
    else
        echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
	FAIL="$FAIL$SHORT "
	LOGS="${LOGS}$TESTLOG "
    fi

done

ELAPSED=$("$HOME/bin/showtime" "$SECONDS")

if [ "$FAIL" != "" ]; then
	echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG
	
	echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP
	for L in $LOGS; do 
		echo "$HOSTNAME:$L" >> $TMP 
		echo "[...]" >> $TMP
		tail -3 $L >> $TMP
		echo >> $TMP
	done
	echo "Have a nice day," >> $TMP
	echo "  isatest" >> $TMP

        for R in $MAILTO; do
	    $MAIL "isabelle test failed" $R $TMP
	done

	rm $TMP

	exit 1
else
        echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG
fi

# end