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