author | kleing |
Sun, 06 Apr 2003 21:16:50 +0200 | |
changeset 13901 | af38553e61ee |
parent 13838 | fe83f2231767 |
child 13924 | 09f6f2fefb25 |
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 |
||
13838 | 54 |
case $HOSTNAME in |
55 |
atbroy51) |
|
56 |
MFLAGS="-j 2" |
|
57 |
# MFLAGS="" |
|
58 |
;; |
|
59 |
||
60 |
atbroy31) |
|
61 |
MFLAGS="-j 5" |
|
62 |
;; |
|
63 |
||
64 |
atbroy12) |
|
65 |
MFLAGS="-j 5" |
|
66 |
;; |
|
67 |
||
68 |
sunbroy2) |
|
69 |
MFLAGS="-j 4" |
|
70 |
;; |
|
71 |
||
13901 | 72 |
sunbroy1) |
73 |
MFLAGS="-j 2" |
|
74 |
;; |
|
75 |
||
13838 | 76 |
*) |
77 |
MFLAGS="" |
|
78 |
;; |
|
79 |
esac |
|
80 |
||
81 |
||
82 |
||
13320 | 83 |
LOGS="" |
84 |
||
13231 | 85 |
for SETTINGS in $@; do |
86 |
||
87 |
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
|
88 |
||
89 |
||
90 |
# logfile setup |
|
91 |
||
13432
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
92 |
DATE=$(date "+%Y-%m-%d") |
13231 | 93 |
SHORT=${SETTINGS##*/} |
94 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
|
95 |
||
96 |
# the test |
|
97 |
||
98 |
echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
|
99 |
||
13233 | 100 |
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
13838 | 101 |
nice $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
13231 | 102 |
|
103 |
if [ $? -eq 0 ] |
|
104 |
then |
|
13236 | 105 |
echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
13231 | 106 |
gzip -f $TESTLOG |
13246 | 107 |
rm -rf ~/isabelle-$SHORT |
13231 | 108 |
else |
109 |
echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
|
13236 | 110 |
FAIL="$FAIL$SHORT " |
13432
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
111 |
LOGS="${LOGS}$TESTLOG " |
13231 | 112 |
fi |
113 |
||
114 |
done |
|
115 |
||
13236 | 116 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
117 |
||
118 |
if [ "$FAIL" != "" ]; then |
|
119 |
echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG |
|
13320 | 120 |
|
121 |
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
|
122 |
for L in $LOGS; do |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
123 |
echo "$HOSTNAME:$L" >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
124 |
echo "[...]" >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
125 |
tail -3 $L >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
126 |
echo >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
127 |
done |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
128 |
echo "Have a nice day," >> $TMP |
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
129 |
echo " isatest" >> $TMP |
13320 | 130 |
|
131 |
for R in $MAILTO; do |
|
132 |
$MAIL "isabelle test failed" $R $TMP |
|
133 |
done |
|
134 |
||
135 |
rm $TMP |
|
136 |
||
13236 | 137 |
exit 1 |
138 |
else |
|
139 |
echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG |
|
140 |
fi |
|
141 |
||
142 |
# end |