# HG changeset patch # User kleing # Date 1114862818 -7200 # Node ID e30f9161890f1f87004a581e8a4315fbb1bb5189 # Parent 435f0e7438543ddb630850ffbafaebe5fd27442d separate test run for theories in Doc/ diff -r 435f0e743854 -r e30f9161890f Admin/isatest-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="kleing@cse.unsw.edu.au" # nipkow@in.tum.de berghofe@in.tum.de lp15@cam.ac.uk" + +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 <> $MASTERLOG +fi +