author | kleing |
Fri, 25 Apr 2003 15:17:36 +0200 | |
changeset 13924 | 09f6f2fefb25 |
parent 13901 | af38553e61ee |
child 13962 | 908f6776a59b |
permissions | -rwxr-xr-x |
13231 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# $Id$ |
|
4 |
# Author: Gerwin Klein, TU Muenchen |
|
5 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6 |
# |
|
7 |
# DESCRIPTION: Run isatool makeall from specified distribution and settings. |
|
8 |
# Send email if it fails. |
|
9 |
||
10 |
## global settings |
|
13838 | 11 |
MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk" |
13246 | 12 |
|
13232 | 13 |
LOGPREFIX=~/log |
13231 | 14 |
|
13236 | 15 |
MASTERLOG=$LOGPREFIX/isatest.log |
16 |
||
13320 | 17 |
TMP=/tmp/isatest-makeall.$$ |
18 |
||
19 |
MAIL=~/bin/pmail |
|
20 |
||
13231 | 21 |
## diagnostics |
22 |
||
23 |
PRG="$(basename "$0")" |
|
24 |
||
25 |
function usage() |
|
26 |
{ |
|
27 |
echo |
|
28 |
echo "Usage: $PRG distributionpath settings1 [settings2 ...]" |
|
29 |
echo |
|
30 |
echo " Run isatool makeall from specified distribution and settings." |
|
31 |
echo " Send email if it fails." |
|
32 |
echo |
|
33 |
exit 1 |
|
34 |
} |
|
35 |
||
36 |
function fail() |
|
37 |
{ |
|
38 |
echo "$1" >&2 |
|
39 |
exit 2 |
|
40 |
} |
|
41 |
||
42 |
## main |
|
43 |
||
44 |
# argument checking |
|
45 |
||
46 |
[ "$1" = "-?" ] && usage |
|
47 |
[ "$#" -lt "2" ] && usage |
|
48 |
||
49 |
DISTPREFIX=$1 |
|
50 |
shift |
|
51 |
||
52 |
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
|
53 |
||
13924 | 54 |
NICE=nice |
55 |
||
13838 | 56 |
case $HOSTNAME in |
57 |
atbroy51) |
|
58 |
MFLAGS="-j 2" |
|
59 |
# MFLAGS="" |
|
13924 | 60 |
NICE="" |
13838 | 61 |
;; |
62 |
||
63 |
atbroy31) |
|
64 |
MFLAGS="-j 5" |
|
65 |
;; |
|
66 |
||
67 |
atbroy12) |
|
68 |
MFLAGS="-j 5" |
|
69 |
;; |
|
70 |
||
71 |
sunbroy2) |
|
72 |
MFLAGS="-j 4" |
|
73 |
;; |
|
74 |
||
13901 | 75 |
sunbroy1) |
76 |
MFLAGS="-j 2" |
|
77 |
;; |
|
78 |
||
13838 | 79 |
*) |
80 |
MFLAGS="" |
|
81 |
;; |
|
82 |
esac |
|
83 |
||
84 |
||
85 |
||
13320 | 86 |
LOGS="" |
87 |
||
13231 | 88 |
for SETTINGS in $@; do |
89 |
||
90 |
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
|
91 |
||
92 |
||
93 |
# logfile setup |
|
94 |
||
13432
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
95 |
DATE=$(date "+%Y-%m-%d") |
13231 | 96 |
SHORT=${SETTINGS##*/} |
97 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
|
98 |
||
99 |
# the test |
|
100 |
||
101 |
echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
|
102 |
||
13233 | 103 |
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
13924 | 104 |
$NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
13231 | 105 |
|
106 |
if [ $? -eq 0 ] |
|
107 |
then |
|
13236 | 108 |
echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
13231 | 109 |
gzip -f $TESTLOG |
13246 | 110 |
rm -rf ~/isabelle-$SHORT |
13231 | 111 |
else |
112 |
echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
|
13236 | 113 |
FAIL="$FAIL$SHORT " |
13432
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
114 |
LOGS="${LOGS}$TESTLOG " |
13231 | 115 |
fi |
116 |
||
117 |
done |
|
118 |
||
13236 | 119 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
120 |
||
121 |
if [ "$FAIL" != "" ]; then |
|
122 |
echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG |
|
13320 | 123 |
|
124 |
echo "Test for platform(s) ${FAIL}failed. Log file(s) available at" > $TMP |
|
13432
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
125 |
for L in $LOGS; do |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
126 |
echo "$HOSTNAME:$L" >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
127 |
echo "[...]" >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
128 |
tail -3 $L >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
129 |
echo >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
130 |
done |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
131 |
echo "Have a nice day," >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
132 |
echo " isatest" >> $TMP |
13320 | 133 |
|
134 |
for R in $MAILTO; do |
|
135 |
$MAIL "isabelle test failed" $R $TMP |
|
136 |
done |
|
137 |
||
138 |
rm $TMP |
|
139 |
||
13236 | 140 |
exit 1 |
141 |
else |
|
142 |
echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG |
|
143 |
fi |
|
144 |
||
145 |
# end |