Admin/isatest/isatest-doc
author wenzelm
Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago)
changeset 28500 4b79e5d3d0aa
parent 28388 0789bbedfc62
child 28504 7ad7d7d6df47
permissions -rwxr-xr-x
replaced ISATOOL by ISABELLE_TOOL;
kleing@22410
     1
#!/usr/bin/env bash
kleing@22410
     2
#
kleing@22410
     3
# $Id$
kleing@22410
     4
# Author: Gerwin Klein, NICTA
kleing@22410
     5
#
kleing@22410
     6
# Run IsaMakefile for every Doc/ subdirectory.
kleing@22410
     7
#
kleing@22410
     8
# Relies on being run in the isatest environment on sunbroy2.
kleing@22410
     9
# 
kleing@22410
    10
kleing@22410
    11
. ~/.bashrc
kleing@22410
    12
kleing@22410
    13
## global settings
kleing@22411
    14
. ~/admin/isatest/isatest-settings
kleing@22410
    15
kleing@22410
    16
DOCDIR=$HOME/Doc
kleing@22410
    17
kleing@22410
    18
MAXTIME=1800
kleing@22410
    19
kleing@22410
    20
ISABELLE_DEVEL=$DISTPREFIX/Isabelle
kleing@22410
    21
DATE=$(date "+%Y-%m-%d")
kleing@22410
    22
kleing@22410
    23
LOG=$LOGPREFIX/isatest-doc-$DATE.log
kleing@22410
    24
isatest@27087
    25
SHORT=at-poly
kleing@22410
    26
SETTINGS=~/settings/$SHORT
kleing@22410
    27
wenzelm@28500
    28
ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isatool
kleing@22410
    29
    
kleing@22410
    30
kleing@22820
    31
MAIL=$HOME/bin/pmail
kleing@22410
    32
kleing@22410
    33
TMP=/tmp/isatest-doc.mail.tmp
kleing@22410
    34
while [ -e $TMP ]; do TMP=$TMP.x; done
kleing@22410
    35
kleing@22410
    36
#
kleing@22410
    37
PRG="$(basename "$0")"
kleing@22410
    38
kleing@22410
    39
## functions
kleing@22410
    40
kleing@22410
    41
function usage()
kleing@22410
    42
{
kleing@22410
    43
  echo
kleing@22410
    44
  echo "Usage: $PRG"
kleing@22410
    45
  echo
kleing@22410
    46
  echo "  Run IsaMakefile for every Doc/ subdirectory"
kleing@22410
    47
  echo 
kleing@22410
    48
  exit 1
kleing@22410
    49
}
kleing@22410
    50
kleing@22410
    51
function fail()
kleing@22410
    52
{
kleing@22410
    53
  echo "$1" >&2
kleing@22410
    54
  exit 2
kleing@22410
    55
}
kleing@22410
    56
kleing@22410
    57
## 
kleing@22410
    58
kleing@22410
    59
[ "$#" != "0" ] && usage
kleing@22410
    60
kleing@22410
    61
if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
kleing@22410
    62
  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
kleing@22410
    63
  exit 1
kleing@22410
    64
fi
kleing@22410
    65
cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
kleing@22410
    66
kleing@22410
    67
kleing@22410
    68
echo "Start test at `date`" > $LOG
kleing@22410
    69
echo >> $LOG
kleing@22410
    70
kleing@22410
    71
cd $DOCDIR || fail "could not cd to $DOCDIR"
kleing@22410
    72
kleing@22410
    73
# run test
kleing@22410
    74
FAIL="";
kleing@22410
    75
kleing@22410
    76
cd $DOCDIR
kleing@22410
    77
for DIR in */; do
kleing@22410
    78
  if [ -f "$DIR/IsaMakefile" ]; then
kleing@22410
    79
    echo "Testing [$DIR]" >> $LOG
kleing@22410
    80
    (
kleing@22410
    81
      cd $DIR
kleing@22410
    82
      ulimit -t $MAXTIME 
wenzelm@28500
    83
      nice $ISABELLE_TOOL make >> $LOG 2>&1
kleing@22410
    84
    ) || FAIL="${FAIL}${DIR} "    
kleing@22410
    85
    echo "Finished [$DIR]" >> $LOG
kleing@22410
    86
    echo >> $LOG
kleing@22410
    87
  fi
kleing@22410
    88
done
kleing@22410
    89
kleing@22410
    90
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
kleing@22410
    91
kleing@22410
    92
echo >> $LOG
kleing@22410
    93
echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
kleing@22410
    94
kleing@22410
    95
# send email if there was a problem
kleing@22410
    96
if [ "$FAIL" != "" ]; then
kleing@22410
    97
  echo >> $LOG
kleing@22410
    98
  echo "Failed sessions: ${FAIL}" >> $LOG
kleing@22410
    99
kleing@22410
   100
  echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
kleing@22410
   101
kleing@22410
   102
  cat > $TMP <<EOF
kleing@22410
   103
Session(s) ${FAIL} in the documentation test failed (log attached).
kleing@22410
   104
Test ended on: $HOSTNAME, `date`.
kleing@22410
   105
kleing@22410
   106
Have a nice day,
kleing@22410
   107
  isatest
kleing@22410
   108
kleing@22410
   109
EOF
kleing@22410
   110
kleing@22410
   111
  for R in $MAILTO; do
kleing@22410
   112
    $MAIL 'doc test failed' "$R" $TMP $LOG
kleing@22410
   113
  done
kleing@22410
   114
kleing@22410
   115
  rm -f $TMP
kleing@22410
   116
kleing@22410
   117
  exit 1
kleing@22410
   118
else
kleing@22410
   119
  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
kleing@22410
   120
fi
kleing@22410
   121