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

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

  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

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

  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