--- a/Admin/isatest-doc Mon Mar 05 10:14:32 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,127 +0,0 @@
-#!/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
-
-## global settings
-. ~/admin/isatest-settings
-
-DOCDIR=$HOME/Doc
-
-MAXTIME=1800
-
-ISABELLE_DEVEL=$DISTPREFIX/Isabelle
-DATE=$(date "+%Y-%m-%d")
-
-LOG=$LOGPREFIX/isatest-doc-$DATE.log
-
-SHORT=sun-poly
-SETTINGS=~/settings/$SHORT
-
-ISATOOL=$ISABELLE_DEVEL/bin/isatool
-
-
-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) ${FAIL} 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
-