Admin/isatest-doc
author haftmann
Sun Jun 05 14:33:02 2005 +0200 (2005-06-05)
changeset 16275 951803bff5b1
parent 15937 b74dfcdeac1b
child 16615 e665dafdd2b8
permissions -rwxr-xr-x
a more spohisticated symlink handling
     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 ## settings
    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"
    15 
    16 DOCDIR=$HOME/Doc
    17 DISTPREFIX=~/tmp/isadist
    18 
    19 MAXTIME=1800
    20 
    21 ISABELLE_DEVEL=$DISTPREFIX/Isabelle
    22 DATE=$(date "+%Y-%m-%d")
    23 
    24 LOG=~/log/isatest-doc-$DATE.log
    25 MASTERLOG=~/log/isatest.log
    26 
    27 SHORT=sun-poly
    28 SETTINGS=~/settings/$SHORT
    29 
    30 ISATOOL=$ISABELLE_DEVEL/bin/isatool
    31     
    32 ERRORDIR=$HOME/var
    33 ERRORLOG=$ERRORDIR/error.log
    34 RUNNING=$HOME/var/running
    35 
    36 MAIL=~/afp/release/admin/mail-attach
    37 
    38 TMP=/tmp/isatest-doc.mail.tmp
    39 while [ -e $TMP ]; do TMP=$TMP.x; done
    40 
    41 #
    42 PRG="$(basename "$0")"
    43 
    44 ## functions
    45 
    46 function usage()
    47 {
    48   echo
    49   echo "Usage: $PRG"
    50   echo
    51   echo "  Run IsaMakefile for every Doc/ subdirectory"
    52   echo 
    53   exit 1
    54 }
    55 
    56 function fail()
    57 {
    58   echo "$1" >&2
    59   exit 2
    60 }
    61 
    62 ## 
    63 
    64 [ "$#" != "0" ] && usage
    65 
    66 if [ -f "$RUNNING/$SHORT.running" -o -e $ERRORLOG ]; then
    67   echo "$(date) $HOSTNAME $PRG: Skipped test. Isabelle devel version broken." >> $MASTERLOG
    68   exit 1
    69 fi
    70 cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
    71 
    72 
    73 echo "Start test at `date`" > $LOG
    74 echo >> $LOG
    75 echo "begin cvs update" >> $LOG
    76 
    77 # cvs update to newest version 
    78 cd $DOCDIR || fail "could not cd to $DOCDIR"
    79 cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
    80 
    81 echo "end cvs update" >> $LOG
    82 echo >> $LOG
    83 
    84 # run test
    85 FAIL="";
    86 
    87 cd $DOCDIR
    88 for DIR in */; do
    89   if [ -f "$DIR/IsaMakefile" ]; then
    90     echo "Testing [$DIR]" >> $LOG
    91     (
    92       cd $DIR
    93       ulimit -t $MAXTIME 
    94       nice $ISATOOL make >> $LOG 2>&1
    95     ) || FAIL="${FAIL}${DIR} "    
    96     echo "Finished [$DIR]" >> $LOG
    97     echo >> $LOG
    98   fi
    99 done
   100 
   101 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
   102 
   103 echo >> $LOG
   104 echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
   105 
   106 # send email if there was a problem
   107 if [ "$FAIL" != "" ]; then
   108   echo >> $LOG
   109   echo "Failed sessions: ${FAIL}" >> $LOG
   110 
   111   echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
   112 
   113   cat > $TMP <<EOF
   114 Session(s) ${FAIL} in the documentation test failed (log attached).
   115 Test ended on: $HOSTNAME, `date`.
   116 
   117 Have a nice day,
   118   isatest
   119 
   120 EOF
   121 
   122   for R in $MAILTO; do
   123     $MAIL 'doc test failed' "$R" $TMP $LOG
   124   done
   125 
   126   rm -f $TMP
   127 
   128   exit 1
   129 else
   130   echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
   131 fi
   132