--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-makeall Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,134 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+#
+# DESCRIPTION: Run isatool makeall from specified distribution and settings.
+
+## global settings
+. ~/admin/isatest-settings
+
+# max time until test is aborted (in sec)
+MAXTIME=28800
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG settings1 [settings2 ...]"
+ echo
+ echo " Runs isatool makeall for specified settings."
+ echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ echo "$(date) $HOSTNAME $PRG: FAILED, $1" >> $MASTERLOG
+ exit 2
+}
+
+## main
+
+# argument checking
+
+[ "$1" = "-?" ] && usage
+[ "$#" -lt "1" ] && usage
+
+[ -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"
+ ;;
+
+ macbroy5)
+ MFLAGS="" # -j 2 does not work on poly/macos 10.4.1
+ 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
+ (ulimit -t $MAXTIME; $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