author | wenzelm |
Sun, 18 Sep 2011 16:33:30 +0200 | |
changeset 44978 | a04f3eb3943c |
parent 41967 | 6aa69999da8f |
child 45861 | 4bb0fc92247b |
permissions | -rwxr-xr-x |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
2 |
# |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
3 |
# Author: Gerwin Klein, TU Muenchen |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
4 |
# |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28500
diff
changeset
|
5 |
# DESCRIPTION: Run isabelle makeall from specified distribution and settings. |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
6 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
7 |
## global settings |
22411 | 8 |
. ~/admin/isatest/isatest-settings |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
9 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
10 |
# max time until test is aborted (in sec) |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
11 |
MAXTIME=28800 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
12 |
|
36133
1d199975ebf9
adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;
wenzelm
parents:
36074
diff
changeset
|
13 |
PUBLISH_TEST="$HOME/home/isabelle-repository/repos/testtool/publish_test.py" |
32505
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
14 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
15 |
## diagnostics |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
16 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
17 |
PRG="$(basename "$0")" |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
18 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
19 |
function usage() |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
20 |
{ |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
21 |
echo |
24753 | 22 |
echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
23 |
echo |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28500
diff
changeset
|
24 |
echo " Runs isabelle makeall for specified settings." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
25 |
echo " Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails." |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
26 |
echo |
24753 | 27 |
echo "Examples:" |
28 |
echo " $PRG ~/settings/at-poly ~/settings/at-sml" |
|
29 |
echo " $PRG -l HOL \"HOL-Library HOL-Bali\" ~/settings/at-poly" |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
30 |
exit 1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
31 |
} |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
32 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
33 |
function fail() |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
34 |
{ |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
35 |
echo "$1" >&2 |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28527
diff
changeset
|
36 |
log "FAILED, $1" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
37 |
exit 2 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
38 |
} |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
39 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
40 |
## main |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
41 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
42 |
# argument checking |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
43 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
44 |
[ "$1" = "-?" ] && usage |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
45 |
[ "$#" -lt "1" ] && usage |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
46 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
47 |
[ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory." |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
48 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
49 |
# make file flags and nice setup for different target platforms |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
50 |
case $HOSTNAME in |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
51 |
atbroy51) |
32165 | 52 |
MFLAGS="-k -j 2" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
53 |
NICE="" |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
54 |
;; |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
55 |
|
24758 | 56 |
atbroy98) |
32165 | 57 |
MFLAGS="-k" |
26369 | 58 |
NICE="" |
59 |
;; |
|
24647 | 60 |
|
36074
6301046146b6
isatest: basic setup for cygwin-poly on atbroy102;
wenzelm
parents:
33214
diff
changeset
|
61 |
atbroy102) |
6301046146b6
isatest: basic setup for cygwin-poly on atbroy102;
wenzelm
parents:
33214
diff
changeset
|
62 |
MFLAGS="-k" |
6301046146b6
isatest: basic setup for cygwin-poly on atbroy102;
wenzelm
parents:
33214
diff
changeset
|
63 |
NICE="" |
6301046146b6
isatest: basic setup for cygwin-poly on atbroy102;
wenzelm
parents:
33214
diff
changeset
|
64 |
;; |
6301046146b6
isatest: basic setup for cygwin-poly on atbroy102;
wenzelm
parents:
33214
diff
changeset
|
65 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
66 |
atbroy31) |
32165 | 67 |
MFLAGS="-k -j 2" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
68 |
;; |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
69 |
|
31581 | 70 |
macbroy2) |
32165 | 71 |
MFLAGS="-k" |
31581 | 72 |
NICE="" |
73 |
;; |
|
74 |
||
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
75 |
macbroy5) |
32165 | 76 |
MFLAGS="-k -j 2" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
77 |
NICE="" |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
78 |
;; |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
79 |
|
44978 | 80 |
macbroy6) |
81 |
MFLAGS="-k" |
|
82 |
NICE="" |
|
83 |
;; |
|
84 |
||
32418 | 85 |
macbroy22) |
32320
8175fda90c46
options for more precise performance figures of at-poly, which happens to run on macbroy21;
wenzelm
parents:
32165
diff
changeset
|
86 |
MFLAGS="-k" |
8175fda90c46
options for more precise performance figures of at-poly, which happens to run on macbroy21;
wenzelm
parents:
32165
diff
changeset
|
87 |
NICE="" |
8175fda90c46
options for more precise performance figures of at-poly, which happens to run on macbroy21;
wenzelm
parents:
32165
diff
changeset
|
88 |
;; |
8175fda90c46
options for more precise performance figures of at-poly, which happens to run on macbroy21;
wenzelm
parents:
32165
diff
changeset
|
89 |
|
37874
954dc0c580bd
reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;
wenzelm
parents:
37160
diff
changeset
|
90 |
macbroy28) |
32165 | 91 |
MFLAGS="-k -j 2" |
31581 | 92 |
NICE="nice" |
31496
c4b74075fc17
no parallel make jobs on macbroy23, which is the machine where SML/XL is tested -- attempt to consume less resources;
wenzelm
parents:
28982
diff
changeset
|
93 |
;; |
c4b74075fc17
no parallel make jobs on macbroy23, which is the machine where SML/XL is tested -- attempt to consume less resources;
wenzelm
parents:
28982
diff
changeset
|
94 |
|
26369 | 95 |
macbroy2[0-9]) |
32165 | 96 |
MFLAGS="-k -j 2" |
26369 | 97 |
NICE="" |
98 |
;; |
|
99 |
||
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
100 |
*) |
32165 | 101 |
MFLAGS="-k" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
102 |
# be nice by default |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
103 |
NICE=nice |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
104 |
;; |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
105 |
esac |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
106 |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28500
diff
changeset
|
107 |
ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle" |
24753 | 108 |
|
28500 | 109 |
[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL" |
24753 | 110 |
|
111 |
if [ "$1" = "-l" ]; then |
|
112 |
shift |
|
113 |
[ "$#" -lt "3" ] && usage |
|
114 |
LOGIC="$1" |
|
115 |
TARGETS="$2" |
|
116 |
shift 2 |
|
28500 | 117 |
ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)" |
24786 | 118 |
DIR="$ISABELLE_HOME/src/$LOGIC" |
28500 | 119 |
TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS" |
24753 | 120 |
else |
24781 | 121 |
DIR="." |
28500 | 122 |
TOOL="$ISABELLE_TOOL makeall $MFLAGS all" |
24753 | 123 |
fi |
124 |
||
32505
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
125 |
IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT") |
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
126 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
127 |
# main test loop |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
128 |
|
28597 | 129 |
log "starting [$@]" |
130 |
||
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
131 |
for SETTINGS in $@; do |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
132 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
133 |
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
134 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
135 |
# logfile setup |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
136 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
137 |
DATE=$(date "+%Y-%m-%d") |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
138 |
SHORT=${SETTINGS##*/} |
28527
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
139 |
|
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
140 |
if [ "${SHORT%-e}" == "$SHORT" ]; then |
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
141 |
# normal test |
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
142 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
143 |
else |
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
144 |
# experimental test |
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
145 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log |
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
146 |
fi |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
147 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
148 |
# the test |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
149 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
150 |
touch $RUNNING/$SHORT.running |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
151 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
152 |
echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
153 |
|
39686 | 154 |
echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1 |
155 |
||
28982 | 156 |
if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then |
157 |
echo "--- cleaning up old $ISABELLE_HOME_USER" |
|
158 |
rm -rf $ISABELLE_HOME_USER |
|
159 |
fi |
|
160 |
||
41967
6aa69999da8f
isatest: fresh copy of settings avoids odd cumulative environment;
wenzelm
parents:
39686
diff
changeset
|
161 |
cp $DISTPREFIX/Isabelle/etc/settings.orig $DISTPREFIX/Isabelle/etc/settings |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
162 |
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
24781 | 163 |
(ulimit -t $MAXTIME; cd $DIR; $NICE $TOOL >> $TESTLOG 2>&1) |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
164 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
165 |
if [ $? -eq 0 ] |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
166 |
then |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
167 |
# test log and cleanup |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
168 |
echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
32505
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
169 |
if [ -x $PUBLISH_TEST ]; then |
32889 | 170 |
$PUBLISH_TEST -r $IDENT -s "SUCCESS" -a log $TESTLOG -n Makeall_isatest_$SHORT |
32505
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
171 |
fi |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
172 |
gzip -f $TESTLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
173 |
else |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
174 |
# test log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
175 |
echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
32505
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
176 |
if [ -x $PUBLISH_TEST ]; then |
32889 | 177 |
$PUBLISH_TEST -r $IDENT -s "FAIL" -a log $TESTLOG -n Makeall_isatest_$SHORT |
32505
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
178 |
fi |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
179 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
180 |
# error log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
181 |
echo "Test for platform ${SHORT} failed. Log file attached." >> $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
182 |
echo "[...]" >> $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
183 |
tail -3 $TESTLOG >> $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
184 |
echo >> $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
185 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
186 |
FAIL="$FAIL$SHORT " |
38434 | 187 |
(cd $ERRORDIR; cp $TESTLOG .) |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
188 |
fi |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
189 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
190 |
rm -f $RUNNING/$SHORT.running |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
191 |
done |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
192 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
193 |
# time and success/failure to master log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
194 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
195 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
196 |
if [ -z "$FAIL" ]; then |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28527
diff
changeset
|
197 |
log "all tests successful, elapsed time $ELAPSED." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
198 |
else |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28527
diff
changeset
|
199 |
log "targets ${FAIL}FAILED, elapsed time $ELAPSED." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
200 |
exit 1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
201 |
fi |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
202 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
203 |
# end |