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