Admin/isatest-doc
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 16615 e665dafdd2b8
permissions -rwxr-xr-x
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
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
16615
e665dafdd2b8 use global settings for isatest-doc
kleing
parents: 15937
diff changeset
    13
## global settings
e665dafdd2b8 use global settings for isatest-doc
kleing
parents: 15937
diff changeset
    14
. ~/admin/isatest-settings
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
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    18
MAXTIME=1800
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    19
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    20
ISABELLE_DEVEL=$DISTPREFIX/Isabelle
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    21
DATE=$(date "+%Y-%m-%d")
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    22
16615
e665dafdd2b8 use global settings for isatest-doc
kleing
parents: 15937
diff changeset
    23
LOG=$LOGPREFIX/isatest-doc-$DATE.log
15899
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    24
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    25
SHORT=sun-poly
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    26
SETTINGS=~/settings/$SHORT
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    27
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    28
ISATOOL=$ISABELLE_DEVEL/bin/isatool
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
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    31
MAIL=~/afp/release/admin/mail-attach
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    32
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    33
TMP=/tmp/isatest-doc.mail.tmp
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    34
while [ -e $TMP ]; do TMP=$TMP.x; done
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
#
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    37
PRG="$(basename "$0")"
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    38
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    39
## functions
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
function usage()
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    42
{
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    43
  echo
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    44
  echo "Usage: $PRG"
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    45
  echo
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    46
  echo "  Run IsaMakefile for every Doc/ subdirectory"
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    47
  echo 
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    48
  exit 1
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    49
}
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    50
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    51
function fail()
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    52
{
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    53
  echo "$1" >&2
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    54
  exit 2
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
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
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    59
[ "$#" != "0" ] && usage
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
if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    62
  echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    63
  exit 1
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    64
fi
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    65
cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    66
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    67
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    68
echo "Start test at `date`" > $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    69
echo >> $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    70
echo "begin cvs update" >> $LOG
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
# cvs update to newest version 
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    73
cd $DOCDIR || fail "could not cd to $DOCDIR"
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    74
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
    75
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    76
echo "end cvs update" >> $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    77
echo >> $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    78
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    79
# run test
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    80
FAIL="";
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    81
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    82
cd $DOCDIR
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    83
for DIR in */; do
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    84
  if [ -f "$DIR/IsaMakefile" ]; then
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    85
    echo "Testing [$DIR]" >> $LOG
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 $DIR
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    88
      ulimit -t $MAXTIME 
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    89
      nice $ISATOOL make >> $LOG 2>&1
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    90
    ) || FAIL="${FAIL}${DIR} "    
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    91
    echo "Finished [$DIR]" >> $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    92
    echo >> $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    93
  fi
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    94
done
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    95
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    96
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    97
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    98
echo >> $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
    99
echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
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
# send email if there was a problem
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   102
if [ "$FAIL" != "" ]; then
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 "Failed sessions: ${FAIL}" >> $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
  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
   107
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   108
  cat > $TMP <<EOF
15900
d6156cb8dc2e fixed typo
kleing
parents: 15899
diff changeset
   109
Session(s) ${FAIL} in the documentation test failed (log attached).
15899
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   110
Test ended on: $HOSTNAME, `date`.
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   111
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   112
Have a nice day,
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   113
  isatest
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   114
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   115
EOF
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
  for R in $MAILTO; do
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   118
    $MAIL 'doc test failed' "$R" $TMP $LOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   119
  done
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   120
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   121
  rm -f $TMP
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   122
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   123
  exit 1
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   124
else
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   125
  echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   126
fi
e30f9161890f separate test run for theories in Doc/
kleing
parents:
diff changeset
   127