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 |
|