| author | bulwahn | 
| Tue, 14 Feb 2012 17:29:53 +0100 | |
| changeset 46477 | db693eb03a3f | 
| parent 31582 | 4753c317d5c1 | 
| permissions | -rwxr-xr-x | 
| 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 | 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 | 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: 
28500diff
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 | 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: 
28504diff
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 | 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: 
28504diff
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: 
28504diff
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 |