separate test run for theories in Doc/

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isatest-doc	Sat Apr 30 14:06:58 2005 +0200
@@ -0,0 +1,132 @@
+#!/usr/bin/env bash
+#
+# $Id$
+# Author: Gerwin Klein, NICTA
+#
+# Run IsaMakefile for every Doc/ subdirectory.
+#
+# Relies on being run in the isatest environment on sunbroy2.
+# 
+
+. ~/.bashrc
+
+## settings
+MAILTO="[e-mail]" # [e-mail] [e-mail] [e-mail]"
+
+DOCDIR=$HOME/Doc
+DISTPREFIX=~/tmp/isadist
+
+MAXTIME=1800
+
+ISABELLE_DEVEL=$DISTPREFIX/Isabelle
+DATE=$(date "+%Y-%m-%d")
+
+LOG=~/log/isatest-doc-$DATE.log
+MASTERLOG=~/log/isatest.log
+
+SHORT=sun-poly
+SETTINGS=~/settings/$SHORT
+
+ISATOOL=$ISABELLE_DEVEL/bin/isatool
+    
+ERRORDIR=$HOME/var
+ERRORLOG=$ERRORDIR/error.log
+RUNNING=$HOME/var/running
+
+MAIL=~/afp/release/admin/mail-attach
+
+TMP=/tmp/isatest-doc.mail.tmp
+while [ -e $TMP ]; do TMP=$TMP.x; done
+
+#
+PRG="$(basename "$0")"
+
+## functions
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG"
+  echo
+  echo "  Run IsaMakefile for every Doc/ subdirectory"
+  echo 
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+## 
+
+[ "$#" != "0" ] && usage
+
+if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
+  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
+  exit 1
+fi
+cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
+
+
+echo "Start test at `date`" > $LOG
+echo >> $LOG
+echo "begin cvs update" >> $LOG
+
+# cvs update to newest version 
+cd $DOCDIR || fail "could not cd to $DOCDIR"
+cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
+
+echo "end cvs update" >> $LOG
+echo >> $LOG
+
+# run test
+FAIL="";
+
+cd $DOCDIR
+for DIR in */; do
+  if [ -f "$DIR/IsaMakefile" ]; then
+    echo "Testing [$DIR]" >> $LOG
+    (
+      cd $DIR
+      ulimit -t $MAXTIME 
+      nice $ISATOOL make >> $LOG 2>&1
+    ) || FAIL="${FAIL}${DIR} "    
+    echo "Finished [$DIR]" >> $LOG
+    echo >> $LOG
+  fi
+done
+
+ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+
+echo >> $LOG
+echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
+
+# send email if there was a problem
+if [ "$FAIL" != "" ]; then
+  echo >> $LOG
+  echo "Failed sessions: ${FAIL}" >> $LOG
+
+  echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
+
+  cat > $TMP <<EOF
+Session(s) ${FAILED} in the documentation test failed (log attached).
+Test ended on: $HOSTNAME, `date`.
+
+Have a nice day,
+  isatest
+
+EOF
+
+  for R in $MAILTO; do
+    $MAIL 'doc test failed' "$R" $TMP $LOG
+  done
+
+  rm -f $TMP
+
+  exit 1
+else
+  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
+fi
+