Admin/isatest-doc

standardized facts;

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