# HG changeset patch
# User kleing
# Date 1024602314 -7200
# Node ID cce28efb260098e104af0b7bbea33e8a9364f4a8
# Parent  c5fad3c40d454a76fdd72df0000eabe61743bf0a
for nightly test builds

diff -r c5fad3c40d45 -r cce28efb2600 Admin/isatest-makeall
--- /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
diff -r c5fad3c40d45 -r cce28efb2600 Admin/isatest-makedist
--- /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