Admin/isatest-doc

Simplified version of Jia's filter. Now all constants are pooled, rather than
relevance being compared against separate clauses. Rejects are no longer noted,
and units cannot be added at the end.

#!/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