author | wenzelm |
Sat, 14 Jul 2012 21:15:41 +0200 | |
changeset 48259 | 1635298d8fe7 |
parent 48258 | 734384f35f8a |
child 48608 | 88ff12baccba |
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 |
|
48259 | 13 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
14 |
## diagnostics |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
15 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
16 |
PRG="$(basename "$0")" |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
17 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
18 |
function usage() |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
19 |
{ |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
20 |
echo |
24753 | 21 |
echo "Usage: $PRG [-l logic targets] settings1 [settings2 ...]" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
22 |
echo |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28500
diff
changeset
|
23 |
echo " Runs isabelle makeall for specified settings." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
24 |
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
|
25 |
echo |
24753 | 26 |
echo "Examples:" |
27 |
echo " $PRG ~/settings/at-poly ~/settings/at-sml" |
|
28 |
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
|
29 |
exit 1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
30 |
} |
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 |
function fail() |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
33 |
{ |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
34 |
echo "$1" >&2 |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28527
diff
changeset
|
35 |
log "FAILED, $1" |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
36 |
exit 2 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
37 |
} |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
38 |
|
48259 | 39 |
|
22410
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 |
|
45861
4bb0fc92247b
some full isatest runs, which include benchmark targets;
wenzelm
parents:
44978
diff
changeset
|
49 |
TARGETS=all |
4bb0fc92247b
some full isatest runs, which include benchmark targets;
wenzelm
parents:
44978
diff
changeset
|
50 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
51 |
# make file flags and nice setup for different target platforms |
48259 | 52 |
MFLAGS="-k" |
53 |
NICE="nice" |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
54 |
case $HOSTNAME in |
48259 | 55 |
macbroy2 | macbroy6 | macbroy30) |
31581 | 56 |
NICE="" |
57 |
;; |
|
48158
68a32e12b999
more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents:
48147
diff
changeset
|
58 |
lxbroy[234]) |
68a32e12b999
more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents:
48147
diff
changeset
|
59 |
MFLAGS="-k -j 2" |
68a32e12b999
more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents:
48147
diff
changeset
|
60 |
NICE="" |
68a32e12b999
more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents:
48147
diff
changeset
|
61 |
;; |
68a32e12b999
more tests on lxbroy[234], which are 4 core Xeon machines;
wenzelm
parents:
48147
diff
changeset
|
62 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
63 |
esac |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
64 |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28500
diff
changeset
|
65 |
ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isabelle" |
24753 | 66 |
|
28500 | 67 |
[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL" |
24753 | 68 |
|
69 |
if [ "$1" = "-l" ]; then |
|
70 |
shift |
|
71 |
[ "$#" -lt "3" ] && usage |
|
72 |
LOGIC="$1" |
|
73 |
TARGETS="$2" |
|
74 |
shift 2 |
|
28500 | 75 |
ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)" |
46004
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45861
diff
changeset
|
76 |
if [ "$LOGIC" = "." ]; then |
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45861
diff
changeset
|
77 |
DIR="." |
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45861
diff
changeset
|
78 |
TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS" |
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45861
diff
changeset
|
79 |
else |
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45861
diff
changeset
|
80 |
DIR="$ISABELLE_HOME/src/$LOGIC" |
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45861
diff
changeset
|
81 |
TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS" |
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45861
diff
changeset
|
82 |
fi |
24753 | 83 |
else |
24781 | 84 |
DIR="." |
45861
4bb0fc92247b
some full isatest runs, which include benchmark targets;
wenzelm
parents:
44978
diff
changeset
|
85 |
TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS" |
24753 | 86 |
fi |
87 |
||
32505
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
88 |
IDENT=$(cat "$DISTPREFIX/ISABELLE_IDENT") |
eb82ed858b84
isatest: collect test results and logs in testdata repository
krauss
parents:
32418
diff
changeset
|
89 |
|
48259 | 90 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
91 |
# main test loop |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
92 |
|
28597 | 93 |
log "starting [$@]" |
94 |
||
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
95 |
for SETTINGS in $@; do |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
96 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
97 |
[ -r $SETTINGS ] || fail "Cannot read $SETTINGS." |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
98 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
99 |
# logfile setup |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
100 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
101 |
DATE=$(date "+%Y-%m-%d") |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
102 |
SHORT=${SETTINGS##*/} |
28527
82b36daff4c1
make the test for experimental sessions in isatest-check actually work
kleing
parents:
28504
diff
changeset
|
103 |
|
48259 | 104 |
if [ "${SHORT%-e}" == "$SHORT" ]; then |
105 |
# normal test |
|
106 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME.log |
|
107 |
else |
|
108 |
# experimental test |
|
109 |
TESTLOG=$LOGPREFIX/isatest-makeall-$SHORT-$DATE-$HOSTNAME-e.log |
|
110 |
fi |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
111 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
112 |
# the test |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
113 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
114 |
touch $RUNNING/$SHORT.running |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
115 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
116 |
echo ------------------- starting test --- `date` --- $HOSTNAME > $TESTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
117 |
|
39686 | 118 |
echo "Isabelle version: $IDENT" >> $TESTLOG 2>&1 |
119 |
||
28982 | 120 |
if [ "${ISABELLE_HOME_USER:0:14}" == "/tmp/isabelle-" ]; then |
121 |
echo "--- cleaning up old $ISABELLE_HOME_USER" |
|
122 |
rm -rf $ISABELLE_HOME_USER |
|
123 |
fi |
|
124 |
||
41967
6aa69999da8f
isatest: fresh copy of settings avoids odd cumulative environment;
wenzelm
parents:
39686
diff
changeset
|
125 |
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
|
126 |
cat $SETTINGS >> $DISTPREFIX/Isabelle/etc/settings |
24781 | 127 |
(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
|
128 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
129 |
if [ $? -eq 0 ] |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
130 |
then |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
131 |
# test log and cleanup |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
132 |
echo ------------------- test successful --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
133 |
gzip -f $TESTLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
134 |
else |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
135 |
# test log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
136 |
echo ------------------- test FAILED --- `date` --- $HOSTNAME >> $TESTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
137 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
138 |
# error log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
139 |
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
|
140 |
echo "[...]" >> $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
141 |
tail -3 $TESTLOG >> $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
142 |
echo >> $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
143 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
144 |
FAIL="$FAIL$SHORT " |
38434 | 145 |
(cd $ERRORDIR; cp $TESTLOG .) |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
146 |
fi |
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 |
rm -f $RUNNING/$SHORT.running |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
149 |
done |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
150 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
151 |
# time and success/failure to master log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
152 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
153 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
154 |
if [ -z "$FAIL" ]; then |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28527
diff
changeset
|
155 |
log "all tests successful, elapsed time $ELAPSED." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
156 |
else |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28527
diff
changeset
|
157 |
log "targets ${FAIL}FAILED, elapsed time $ELAPSED." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
158 |
exit 1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
159 |
fi |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
160 |