Admin/isatest-doc
author kleing
Sat Apr 30 14:06:58 2005 +0200 (2005-04-30)
changeset 15899 e30f9161890f
child 15900 d6156cb8dc2e
permissions -rwxr-xr-x
separate test run for theories in Doc/
kleing@15899
     1
#!/usr/bin/env bash
kleing@15899
     2
#
kleing@15899
     3
# $Id$
kleing@15899
     4
# Author: Gerwin Klein, NICTA
kleing@15899
     5
#
kleing@15899
     6
# Run IsaMakefile for every Doc/ subdirectory.
kleing@15899
     7
#
kleing@15899
     8
# Relies on being run in the isatest environment on sunbroy2.
kleing@15899
     9
# 
kleing@15899
    10
kleing@15899
    11
. ~/.bashrc
kleing@15899
    12
kleing@15899
    13
## settings
kleing@15899
    14
MAILTO="kleing@cse.unsw.edu.au" # nipkow@in.tum.de berghofe@in.tum.de lp15@cam.ac.uk"
kleing@15899
    15
kleing@15899
    16
DOCDIR=$HOME/Doc
kleing@15899
    17
DISTPREFIX=~/tmp/isadist
kleing@15899
    18
kleing@15899
    19
MAXTIME=1800
kleing@15899
    20
kleing@15899
    21
ISABELLE_DEVEL=$DISTPREFIX/Isabelle
kleing@15899
    22
DATE=$(date "+%Y-%m-%d")
kleing@15899
    23
kleing@15899
    24
LOG=~/log/isatest-doc-$DATE.log
kleing@15899
    25
MASTERLOG=~/log/isatest.log
kleing@15899
    26
kleing@15899
    27
SHORT=sun-poly
kleing@15899
    28
SETTINGS=~/settings/$SHORT
kleing@15899
    29
kleing@15899
    30
ISATOOL=$ISABELLE_DEVEL/bin/isatool
kleing@15899
    31
    
kleing@15899
    32
ERRORDIR=$HOME/var
kleing@15899
    33
ERRORLOG=$ERRORDIR/error.log
kleing@15899
    34
RUNNING=$HOME/var/running
kleing@15899
    35
kleing@15899
    36
MAIL=~/afp/release/admin/mail-attach
kleing@15899
    37
kleing@15899
    38
TMP=/tmp/isatest-doc.mail.tmp
kleing@15899
    39
while [ -e $TMP ]; do TMP=$TMP.x; done
kleing@15899
    40
kleing@15899
    41
#
kleing@15899
    42
PRG="$(basename "$0")"
kleing@15899
    43
kleing@15899
    44
## functions
kleing@15899
    45
kleing@15899
    46
function usage()
kleing@15899
    47
{
kleing@15899
    48
  echo
kleing@15899
    49
  echo "Usage: $PRG"
kleing@15899
    50
  echo
kleing@15899
    51
  echo "  Run IsaMakefile for every Doc/ subdirectory"
kleing@15899
    52
  echo 
kleing@15899
    53
  exit 1
kleing@15899
    54
}
kleing@15899
    55
kleing@15899
    56
function fail()
kleing@15899
    57
{
kleing@15899
    58
  echo "$1" >&2
kleing@15899
    59
  exit 2
kleing@15899
    60
}
kleing@15899
    61
kleing@15899
    62
## 
kleing@15899
    63
kleing@15899
    64
[ "$#" != "0" ] && usage
kleing@15899
    65
kleing@15899
    66
if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
kleing@15899
    67
  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
kleing@15899
    68
  exit 1
kleing@15899
    69
fi
kleing@15899
    70
cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
kleing@15899
    71
kleing@15899
    72
kleing@15899
    73
echo "Start test at `date`" > $LOG
kleing@15899
    74
echo >> $LOG
kleing@15899
    75
echo "begin cvs update" >> $LOG
kleing@15899
    76
kleing@15899
    77
# cvs update to newest version 
kleing@15899
    78
cd $DOCDIR || fail "could not cd to $DOCDIR"
kleing@15899
    79
cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
kleing@15899
    80
kleing@15899
    81
echo "end cvs update" >> $LOG
kleing@15899
    82
echo >> $LOG
kleing@15899
    83
kleing@15899
    84
# run test
kleing@15899
    85
FAIL="";
kleing@15899
    86
kleing@15899
    87
cd $DOCDIR
kleing@15899
    88
for DIR in */; do
kleing@15899
    89
  if [ -f "$DIR/IsaMakefile" ]; then
kleing@15899
    90
    echo "Testing [$DIR]" >> $LOG
kleing@15899
    91
    (
kleing@15899
    92
      cd $DIR
kleing@15899
    93
      ulimit -t $MAXTIME 
kleing@15899
    94
      nice $ISATOOL make >> $LOG 2>&1
kleing@15899
    95
    ) || FAIL="${FAIL}${DIR} "    
kleing@15899
    96
    echo "Finished [$DIR]" >> $LOG
kleing@15899
    97
    echo >> $LOG
kleing@15899
    98
  fi
kleing@15899
    99
done
kleing@15899
   100
kleing@15899
   101
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
kleing@15899
   102
kleing@15899
   103
echo >> $LOG
kleing@15899
   104
echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
kleing@15899
   105
kleing@15899
   106
# send email if there was a problem
kleing@15899
   107
if [ "$FAIL" != "" ]; then
kleing@15899
   108
  echo >> $LOG
kleing@15899
   109
  echo "Failed sessions: ${FAIL}" >> $LOG
kleing@15899
   110
kleing@15899
   111
  echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
kleing@15899
   112
kleing@15899
   113
  cat > $TMP <<EOF
kleing@15899
   114
Session(s) ${FAILED} in the documentation test failed (log attached).
kleing@15899
   115
Test ended on: $HOSTNAME, `date`.
kleing@15899
   116
kleing@15899
   117
Have a nice day,
kleing@15899
   118
  isatest
kleing@15899
   119
kleing@15899
   120
EOF
kleing@15899
   121
kleing@15899
   122
  for R in $MAILTO; do
kleing@15899
   123
    $MAIL 'doc test failed' "$R" $TMP $LOG
kleing@15899
   124
  done
kleing@15899
   125
kleing@15899
   126
  rm -f $TMP
kleing@15899
   127
kleing@15899
   128
  exit 1
kleing@15899
   129
else
kleing@15899
   130
  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
kleing@15899
   131
fi
kleing@15899
   132