author | kleing |
Sat, 06 Dec 2003 04:32:28 +0100 | |
changeset 14280 | d7c3691008f9 |
parent 14279 | 00eb40463c27 |
child 14433 | f25291a96e17 |
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. |
|
13962
908f6776a59b
use /usr/stud/isatest as home for all platforms (macbroy33 has no /home/stud/..)
kleing
parents:
13924
diff
changeset
|
8 |
|
13231 | 9 |
## global settings |
13246 | 10 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
11 |
# canoncical home for all platforms |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
12 |
HOME=/usr/stud/isatest |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
13 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
14 |
# where the log files are |
13962
908f6776a59b
use /usr/stud/isatest as home for all platforms (macbroy33 has no /home/stud/..)
kleing
parents:
13924
diff
changeset
|
15 |
LOGPREFIX=$HOME/log |
13236 | 16 |
MASTERLOG=$LOGPREFIX/isatest.log |
14035 | 17 |
ERRORDIR=$HOME/var |
18 |
ERRORLOG=$ERRORDIR/error.log |
|
13236 | 19 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
20 |
# where to put test-is-running files |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
21 |
RUNNING=$HOME/var/running |
13320 | 22 |
|
23 |
||
13231 | 24 |
## diagnostics |
25 |
||
26 |
PRG="$(basename "$0")" |
|
27 |
||
28 |
function usage() |
|
29 |
{ |
|
30 |
echo |
|
31 |
echo "Usage: $PRG distributionpath settings1 [settings2 ...]" |
|
32 |
echo |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
33 |
echo " Runs isatool makeall from specified distribution and settings." |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
34 |
echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails." |
13231 | 35 |
echo |
36 |
exit 1 |
|
37 |
} |
|
38 |
||
39 |
function fail() |
|
40 |
{ |
|
41 |
echo "$1" >&2 |
|
42 |
exit 2 |
|
43 |
} |
|
44 |
||
45 |
## main |
|
46 |
||
47 |
# argument checking |
|
48 |
||
49 |
[ "$1" = "-?" ] && usage |
|
50 |
[ "$#" -lt "2" ] && usage |
|
51 |
||
52 |
DISTPREFIX=$1 |
|
53 |
shift |
|
54 |
||
55 |
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
|
56 |
||
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
57 |
# make file flags and nice setup for different target platforms |
13838 | 58 |
case $HOSTNAME in |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
59 |
atbroy51) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
60 |
# 2 processors |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
61 |
MFLAGS="-j 2" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
62 |
# MFLAGS="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
63 |
NICE="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
64 |
;; |
13838 | 65 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
66 |
atbroy31) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
67 |
# cluster |
13838 | 68 |
MFLAGS="-j 5" |
69 |
;; |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
70 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
71 |
sunbroy2) |
13990 | 72 |
MFLAGS="-j 6" |
14012 | 73 |
NICE="nice" |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
74 |
;; |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
75 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
76 |
sunbroy1) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
77 |
MFLAGS="-j 2" |
14012 | 78 |
NICE="nice" |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
79 |
;; |
13838 | 80 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
81 |
macbroy*) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
82 |
MFLAGS="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
83 |
NICE="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
84 |
;; |
13838 | 85 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
86 |
*) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
87 |
MFLAGS="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
88 |
# be nice by default |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
89 |
NICE=nice |
13838 | 90 |
;; |
91 |
esac |
|
92 |
||
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
93 |
# main test loop |
13320 | 94 |
|
13231 | 95 |
for SETTINGS in $@; do |
96 |
||
97 |
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
|
98 |
||
99 |
# logfile setup |
|
100 |
||
13432
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
101 |
DATE=$(date "+%Y-%m-%d") |
13231 | 102 |
SHORT=${SETTINGS##*/} |
103 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
|
104 |
||
105 |
# the test |
|
106 |
||
13987 | 107 |
touch $RUNNING/$SHORT.running |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
108 |
|
13231 | 109 |
echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
110 |
||
13233 | 111 |
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
13924 | 112 |
$NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1 |
13231 | 113 |
|
114 |
if [ $? -eq 0 ] |
|
115 |
then |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
116 |
# test log and cleanup |
13236 | 117 |
echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
13231 | 118 |
gzip -f $TESTLOG |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
119 |
rm -rf $HOME/isabelle-$SHORT |
13231 | 120 |
else |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
121 |
# test log |
13231 | 122 |
echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
123 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
124 |
# error log |
14035 | 125 |
echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
126 |
echo "[...]" >> $ERRORLOG |
14035 | 127 |
tail -3 $TESTLOG >> $ERRORLOG |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
128 |
echo >> $ERRORLOG |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
129 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
130 |
FAIL="$FAIL$SHORT " |
14035 | 131 |
(cd $ERRORDIR; ln -s $TESTLOG) |
13231 | 132 |
fi |
133 |
||
13987 | 134 |
rm -f $RUNNING/$SHORT.running |
13231 | 135 |
done |
136 |
||
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
137 |
# time and success/failure to master log |
13236 | 138 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
139 |
||
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
140 |
if [ -z "$FAIL" ]; then |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
141 |
echo "$(date) $HOSTNAME $PRG: all tests successful, elapsed time $ELAPSED." >> $MASTERLOG |
13236 | 142 |
else |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
143 |
echo "$(date) $HOSTNAME $PRG: targets ${FAIL}FAILED, elapsed time $ELAPSED." >> $MASTERLOG |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
144 |
exit 1 |
13236 | 145 |
fi |
146 |
||
147 |
# end |