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