--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest-makeall Thu Jun 20 21:45:14 2002 +0200
@@ -0,0 +1,76 @@
+#!/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
+LOGPREFIX=~
+
+## 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."
+
+for SETTINGS in $@; do
+
+ [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
+
+
+ # logfile setup
+
+ DATE=$(date "+%d-%b-%Y")
+ SHORT=${SETTINGS##*/}
+ TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log
+
+ # the test
+
+ echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1
+
+ cp -v $SETTINGS $DISTPREFIX/Isabelle/etc/settings >> $TESTLOG 2>&1
+ $DISTPREFIX/Isabelle/bin/isatool makeall all >> $TESTLOG 2>&1
+
+ if [ $? -eq 0 ]
+ then
+ echo ------------------- test successfull --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+ gzip -f $TESTLOG
+ else
+ echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1
+ # more action here
+ exit 1
+ fi
+
+done
+
+# end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest-makedist Thu Jun 20 21:45:14 2002 +0200
@@ -0,0 +1,78 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
+
+## global settings
+LOGPREFIX=~
+DISTPREFIX=~/isadist
+MAKEDIST=~/bin/makedist
+
+SUN=sunbroy2
+AT=atbroy37
+
+SSH="ssh -1 -f"
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG"
+ echo
+ echo " Build distribution and run isatest-make for lots of platforms."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+## main
+
+export DISTPREFIX
+
+DATE=$(date "+%d-%b-%Y")
+DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
+
+# get newest version of makedist:
+# cvs -d sunbroy2:/usr/proj/isabelle-repository/archive co isabelle/Admin > $COUTLOG
+
+echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
+
+echo "### cleaning up old dist directory" >> $DISTLOG 2>&1
+rm -rf $DISTPREFIX >> $DISTLOG 2>&1
+
+echo "### building distribution" >> $DISTLOG 2>&1
+$MAKEDIST - >> $DISTLOG 2>&1
+
+if [ $? -ne 0 ]
+then
+ echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
+ # more action here
+ exit 1
+fi
+
+cd $DISTPREFIX >> $DISTLOG 2>&1
+tar xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
+
+echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
+
+## spawn test runs
+
+# run tests in parallel on multiprocessor sun
+$SSH $SUN sun-poly
+$SSH $SUN sun-sml
+
+# run tests sequentially on x86
+$SSH $AT at-poly at-sml
+
+## end
\ No newline at end of file