Admin/isatest-doc
author wenzelm
Tue Jul 05 16:49:15 2005 +0200 (2005-07-05)
changeset 16693 75f39d66425d
parent 16615 e665dafdd2b8
permissions -rwxr-xr-x
fixed regexp grouping;
     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-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=sun-poly
    26 SETTINGS=~/settings/$SHORT
    27 
    28 ISATOOL=$ISABELLE_DEVEL/bin/isatool
    29     
    30 
    31 MAIL=~/afp/release/admin/mail-attach
    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 echo "begin cvs update" >> $LOG
    71 
    72 # cvs update to newest version 
    73 cd $DOCDIR || fail "could not cd to $DOCDIR"
    74 cvs -q up -A -P -d >> $LOG 2>&1 || fail "could not CVS update."
    75 
    76 echo "end cvs update" >> $LOG
    77 echo >> $LOG
    78 
    79 # run test
    80 FAIL="";
    81 
    82 cd $DOCDIR
    83 for DIR in */; do
    84   if [ -f "$DIR/IsaMakefile" ]; then
    85     echo "Testing [$DIR]" >> $LOG
    86     (
    87       cd $DIR
    88       ulimit -t $MAXTIME 
    89       nice $ISATOOL make >> $LOG 2>&1
    90     ) || FAIL="${FAIL}${DIR} "    
    91     echo "Finished [$DIR]" >> $LOG
    92     echo >> $LOG
    93   fi
    94 done
    95 
    96 ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    97 
    98 echo >> $LOG
    99 echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
   100 
   101 # send email if there was a problem
   102 if [ "$FAIL" != "" ]; then
   103   echo >> $LOG
   104   echo "Failed sessions: ${FAIL}" >> $LOG
   105 
   106   echo "$(date) $HOSTNAME $PRG: doc test FAILED for ${FAIL}, elapsed time $ELAPSED." >> $MASTERLOG
   107 
   108   cat > $TMP <<EOF
   109 Session(s) ${FAIL} in the documentation test failed (log attached).
   110 Test ended on: $HOSTNAME, `date`.
   111 
   112 Have a nice day,
   113   isatest
   114 
   115 EOF
   116 
   117   for R in $MAILTO; do
   118     $MAIL 'doc test failed' "$R" $TMP $LOG
   119   done
   120 
   121   rm -f $TMP
   122 
   123   exit 1
   124 else
   125   echo "$(date) $HOSTNAME $PRG: doc test successful, elapsed time $ELAPSED." >> $MASTERLOG
   126 fi
   127