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