Admin/isatest/isatest-doc

do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p"

#!/usr/bin/env bash
#
# 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/isatest-settings

DOCDIR=$HOME/Doc

MAXTIME=1800

ISABELLE_DEVEL=$DISTPREFIX/Isabelle
DATE=$(date "+%Y-%m-%d")

LOG=$LOGPREFIX/isatest-doc-$DATE.log

SHORT=at-poly
SETTINGS=~/settings/$SHORT

ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isabelle
    

MAIL=$HOME/bin/pmail

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
  log "Skipped test. Isabelle devel version broken."
  exit 1
fi
cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings


echo "Start test at `date`" > $LOG
echo >> $LOG

cd $DOCDIR || fail "could not cd to $DOCDIR"

# run test
FAIL="";

cd $DOCDIR
for DIR in */; do
  if [ -f "$DIR/IsaMakefile" ]; then
    echo "Testing [$DIR]" >> $LOG
    (
      cd $DIR
      ulimit -t $MAXTIME 
      nice $ISABELLE_TOOL 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

  log "doc test FAILED for ${FAIL}, elapsed time $ELAPSED."

  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
  log "doc test successful, elapsed time $ELAPSED."
fi