Admin/isatest/isatest-doc

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

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