author | isatest |
Sat, 30 Apr 2005 13:09:38 +0200 | |
changeset 15897 | 86d510b0e4b7 |
parent 15888 | 64533471eec4 |
child 16095 | f6af6b265d20 |
permissions | -rwxr-xr-x |
13231 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# $Id$ |
|
4 |
# Author: Gerwin Klein, TU Muenchen |
|
5 |
# |
|
6 |
# 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
|
7 |
|
13231 | 8 |
## global settings |
13246 | 9 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
10 |
# canoncical home for all platforms |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
11 |
HOME=/usr/stud/isatest |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
12 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
13 |
# 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
|
14 |
LOGPREFIX=$HOME/log |
13236 | 15 |
MASTERLOG=$LOGPREFIX/isatest.log |
14035 | 16 |
ERRORDIR=$HOME/var |
17 |
ERRORLOG=$ERRORDIR/error.log |
|
13236 | 18 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
19 |
# 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
|
20 |
RUNNING=$HOME/var/running |
13320 | 21 |
|
15888 | 22 |
# max time until test is aborted (in sec) |
23 |
MAXTIME=28800 |
|
13320 | 24 |
|
13231 | 25 |
## diagnostics |
26 |
||
27 |
PRG="$(basename "$0")" |
|
28 |
||
29 |
function usage() |
|
30 |
{ |
|
31 |
echo |
|
32 |
echo "Usage: $PRG distributionpath settings1 [settings2 ...]" |
|
33 |
echo |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
34 |
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
|
35 |
echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails." |
13231 | 36 |
echo |
37 |
exit 1 |
|
38 |
} |
|
39 |
||
40 |
function fail() |
|
41 |
{ |
|
42 |
echo "$1" >&2 |
|
43 |
exit 2 |
|
44 |
} |
|
45 |
||
46 |
## main |
|
47 |
||
48 |
# argument checking |
|
49 |
||
50 |
[ "$1" = "-?" ] && usage |
|
51 |
[ "$#" -lt "2" ] && usage |
|
52 |
||
53 |
DISTPREFIX=$1 |
|
54 |
shift |
|
55 |
||
56 |
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
|
57 |
||
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
58 |
# make file flags and nice setup for different target platforms |
13838 | 59 |
case $HOSTNAME in |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
60 |
atbroy51) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
61 |
# 2 processors |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
62 |
MFLAGS="-j 2" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
63 |
# MFLAGS="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
64 |
NICE="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
65 |
;; |
13838 | 66 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
67 |
atbroy31) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
68 |
# cluster |
13838 | 69 |
MFLAGS="-j 5" |
70 |
;; |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
71 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
72 |
sunbroy2) |
13990 | 73 |
MFLAGS="-j 6" |
14012 | 74 |
NICE="nice" |
13985
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 |
|
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
77 |
sunbroy1) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
78 |
MFLAGS="-j 2" |
14012 | 79 |
NICE="nice" |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
80 |
;; |
13838 | 81 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
82 |
macbroy*) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
83 |
MFLAGS="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
84 |
NICE="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
85 |
;; |
13838 | 86 |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
87 |
*) |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
88 |
MFLAGS="" |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
89 |
# be nice by default |
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
90 |
NICE=nice |
13838 | 91 |
;; |
92 |
esac |
|
93 |
||
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
94 |
# main test loop |
13320 | 95 |
|
13231 | 96 |
for SETTINGS in $@; do |
97 |
||
98 |
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
|
99 |
||
100 |
# logfile setup |
|
101 |
||
13432
470daa444967
- changed date format for proper lexicographical ordering
isatest
parents:
13359
diff
changeset
|
102 |
DATE=$(date "+%Y-%m-%d") |
13231 | 103 |
SHORT=${SETTINGS##*/} |
104 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
|
105 |
||
106 |
# the test |
|
107 |
||
13987 | 108 |
touch $RUNNING/$SHORT.running |
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
109 |
|
13231 | 110 |
echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
111 |
||
13233 | 112 |
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
15888 | 113 |
(ulimit -t $MAXTIME; $NICE $DISTPREFIX/Isabelle/bin/isatool makeall $MFLAGS all >> $TESTLOG 2>&1) |
13231 | 114 |
|
115 |
if [ $? -eq 0 ] |
|
116 |
then |
|
13985
3852929a8d1d
leave error messages in error.log, send only one email for all platforms
kleing
parents:
13962
diff
changeset
|
117 |
# test log and cleanup |
13236 | 118 |
echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
13231 | 119 |
gzip -f $TESTLOG |
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 |