diff -r 5f7c9c82b05e -r da313b67a04d Admin/isatest/isatest-makedist
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest/isatest-makedist	Mon Mar 05 22:12:20 2007 +0100
@@ -0,0 +1,112 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, TU Muenchen
+#
+# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
+
+## global settings
+. ~/admin/isatest-settings
+
+TMP=/tmp/isatest-makedist.$$
+MAIL=$HOME/bin/pmail
+
+MAKEDIST=$HOME/bin/makedist
+MAKEALL=$HOME/bin/isatest-makeall
+TAR=gtar
+CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"
+
+SSH="ssh -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
+
+# cleanup old error log and test-still-running files
+rm -f $ERRORLOG
+rm -f $ERRORDIR/isatest-*.log
+rm -f $RUNNING/*.runnning
+
+export DISTPREFIX
+export CVS2CL
+
+DATE=$(date "+%Y-%m-%d")
+DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
+
+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 "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
+rm -rf $HOME/isabelle-*
+
+echo "### building distribution"  >> $DISTLOG 2>&1
+mkdir -p $DISTPREFIX
+$MAKEDIST - >> $DISTLOG 2>&1
+
+if [ $? -ne 0 ]
+then
+    echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
+    ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+    echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
+
+    echo "Could not build isabelle distribution. Log file available at" > $TMP
+    echo "$HOSTNAME:$DISTLOG" >> $TMP
+
+    for R in $MAILTO; do
+        $MAIL "isabelle dist build failed" $R $TMP
+    done
+
+    rm $TMP
+
+    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
+
+ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
+
+
+## spawn test runs
+
+$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
+# give test some time to copy settings and start
+sleep 5
+$SSH atbroy51 "$MAKEALL $HOME/settings/at-poly $HOME/settings/at-poly-e"
+sleep 5
+$SSH atbroy10 "$MAKEALL $HOME/settings/at-sml-dev"
+sleep 5
+$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly-e"
+sleep 5
+$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly $HOME/settings/mac-sml-dev"
+sleep 5
+$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-e"
+
+echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
+
+gzip -f $DISTLOG
+
+## end