3 # $Id$ |
3 # $Id$ |
4 # Author: Gerwin Klein, TU Muenchen |
4 # Author: Gerwin Klein, TU Muenchen |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 # |
6 # |
7 # DESCRIPTION: Run isatool makeall from specified distribution and settings. |
7 # DESCRIPTION: Run isatool makeall from specified distribution and settings. |
8 # Send email if it fails. |
|
9 |
8 |
10 # canoncical home for all platforms |
9 ## global settings |
|
10 |
|
11 # canoncical home for all platforms |
11 HOME=/usr/stud/isatest |
12 HOME=/usr/stud/isatest |
12 |
13 |
13 ## global settings |
14 # where the log files are |
14 MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk" |
15 LOGPREFIX=$HOME/log |
|
16 MASTERLOG=$LOGPREFIX/isatest.log |
|
17 ERRORLOG=$HOME/var/error.log |
15 |
18 |
16 LOGPREFIX=$HOME/log |
19 # where to put test-is-running files |
|
20 RUNNING=$HOME/var/running |
17 |
21 |
18 MASTERLOG=$LOGPREFIX/isatest.log |
|
19 |
|
20 TMP=/tmp/isatest-makeall.$$ |
|
21 |
|
22 MAIL=$HOME/bin/pmail |
|
23 |
22 |
24 ## diagnostics |
23 ## diagnostics |
25 |
24 |
26 PRG="$(basename "$0")" |
25 PRG="$(basename "$0")" |
27 |
26 |
28 function usage() |
27 function usage() |
29 { |
28 { |
30 echo |
29 echo |
31 echo "Usage: $PRG distributionpath settings1 [settings2 ...]" |
30 echo "Usage: $PRG distributionpath settings1 [settings2 ...]" |
32 echo |
31 echo |
33 echo " Run isatool makeall from specified distribution and settings." |
32 echo " Runs isatool makeall from specified distribution and settings." |
34 echo " Send email if it fails." |
33 echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails." |
35 echo |
34 echo |
36 exit 1 |
35 exit 1 |
37 } |
36 } |
38 |
37 |
39 function fail() |
38 function fail() |
52 DISTPREFIX=$1 |
51 DISTPREFIX=$1 |
53 shift |
52 shift |
54 |
53 |
55 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
54 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
56 |
55 |
57 NICE=nice |
56 # make file flags and nice setup for different target platforms |
|
57 case $HOSTNAME in |
|
58 atbroy51) |
|
59 # 2 processors |
|
60 MFLAGS="-j 2" |
|
61 # MFLAGS="" |
|
62 NICE="" |
|
63 ;; |
58 |
64 |
59 case $HOSTNAME in |
65 atbroy31) |
60 atbroy51) |
66 # cluster |
61 MFLAGS="-j 2" |
|
62 # MFLAGS="" |
|
63 NICE="" |
|
64 ;; |
|
65 |
|
66 atbroy31) |
|
67 MFLAGS="-j 5" |
67 MFLAGS="-j 5" |
68 ;; |
68 ;; |
69 |
69 |
70 atbroy12) |
70 sunbroy2) |
71 MFLAGS="-j 5" |
71 MFLAGS="-j 4" |
72 ;; |
72 ;; |
73 |
73 |
74 sunbroy2) |
74 sunbroy1) |
75 MFLAGS="-j 4" |
75 MFLAGS="-j 2" |
76 ;; |
76 ;; |
77 |
77 |
78 sunbroy1) |
78 macbroy*) |
79 MFLAGS="-j 2" |
79 MFLAGS="" |
80 ;; |
80 NICE="" |
|
81 ;; |
81 |
82 |
82 *) |
83 *) |
83 MFLAGS="" |
84 MFLAGS="" |
|
85 # be nice by default |
|
86 NICE=nice |
84 ;; |
87 ;; |
85 esac |
88 esac |
86 |
89 |
87 |
90 # main test loop |
88 |
|
89 LOGS="" |
|
90 |
91 |
91 for SETTINGS in $@; do |
92 for SETTINGS in $@; do |
92 |
93 |
93 [ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
94 [ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
94 |
|
95 |
95 |
96 # logfile setup |
96 # logfile setup |
97 |
97 |
98 DATE=$(date "+%Y-%m-%d") |
98 DATE=$(date "+%Y-%m-%d") |
99 SHORT=${SETTINGS##*/} |
99 SHORT=${SETTINGS##*/} |
100 TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
100 TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
101 |
101 |
102 # the test |
102 # the test |
103 |
103 |
|
104 touch $RUNNING/$SHORT |
|
105 |
104 echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
106 echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
105 |
107 |
106 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
108 cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
107 $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
109 $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
108 |
110 |
109 if [ $? -eq 0 ] |
111 if [ $? -eq 0 ] |
110 then |
112 then |
|
113 # test log and cleanup |
111 echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
114 echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
112 gzip -f $TESTLOG |
115 gzip -f $TESTLOG |
113 rm -rf $HOME/isabelle-$SHORT |
116 rm -rf $HOME/isabelle-$SHORT |
114 else |
117 else |
|
118 # test log |
115 echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
119 echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
116 FAIL="$FAIL$SHORT " |
120 |
117 LOGS="${LOGS}$TESTLOG " |
121 # error log |
|
122 echo "Test for platform ${SHORT}failed. Log file available at" >> $ERRORLOG |
|
123 echo "$HOSTNAME:$TESTLOG" >> $ERRORLOG |
|
124 echo "[...]" >> $ERRORLOG |
|
125 tail -3 $L >> $ERRORLOG |
|
126 echo >> $ERRORLOG |
|
127 |
|
128 FAIL="$FAIL$SHORT " |
118 fi |
129 fi |
119 |
130 |
|
131 rm -f $RUNNING/$SHORT |
120 done |
132 done |
121 |
133 |
|
134 # time and success/failure to master log |
122 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
135 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
123 |
136 |
124 if [ "$FAIL" != "" ]; then |
137 if [ -z "$FAIL" ]; then |
125 echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG |
138 echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG |
126 |
|
127 echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP |
|
128 for L in $LOGS; do |
|
129 echo "$HOSTNAME:$L" >> $TMP |
|
130 echo "[...]" >> $TMP |
|
131 tail -3 $L >> $TMP |
|
132 echo >> $TMP |
|
133 done |
|
134 echo "Have a nice day," >> $TMP |
|
135 echo " isatest" >> $TMP |
|
136 |
|
137 for R in $MAILTO; do |
|
138 $MAIL "isabelle test failed" $R $TMP |
|
139 done |
|
140 |
|
141 rm $TMP |
|
142 |
|
143 exit 1 |
|
144 else |
139 else |
145 echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG |
140 echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG |
|
141 exit 1 |
146 fi |
142 fi |
147 |
143 |
148 # end |
144 # end |