|
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 berghofe@in.tum.de lp15@cam.ac.uk" |
|
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) ${FAILED} 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 |