author | blanchet |
Mon, 28 Apr 2014 00:54:30 +0200 | |
changeset 56765 | 644f0d4820a1 |
parent 53685 | 983711bc98e0 |
child 56997 | ab28906b54ae |
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 |
# |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
5 |
# DESCRIPTION: Build distribution and run isatest-make for lots of platforms. |
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 |
49004 | 8 |
. "$HOME/hg-isabelle/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 |
TMP=/tmp/isatest-makedist.$$ |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
11 |
MAIL=$HOME/bin/pmail |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
12 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
13 |
MAKEALL=$HOME/bin/isatest-makeall |
27084 | 14 |
TAR=tar |
22410
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 |
SSH="ssh -f" |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
17 |
|
48259 | 18 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
19 |
## diagnostics |
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 |
PRG="$(basename "$0")" |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
22 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
23 |
function usage() |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
24 |
{ |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
25 |
echo |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
26 |
echo "Usage: $PRG" |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
27 |
echo |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
28 |
echo " Build distribution and run isatest-make for lots of platforms." |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
29 |
echo |
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 |
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 |
# cleanup old error log and test-still-running files |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
43 |
rm -f $ERRORLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
44 |
rm -f $ERRORDIR/isatest-*.log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
45 |
rm -f $RUNNING/*.runnning |
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 |
export DISTPREFIX |
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 |
DATE=$(date "+%Y-%m-%d") |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
50 |
DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
51 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
52 |
echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
53 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
54 |
echo "### cleaning up old dist directory" >> $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
55 |
rm -rf $DISTPREFIX >> $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
56 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
57 |
echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
58 |
rm -rf $HOME/isabelle-* |
48210
08cb859c53cd
removed switched-off atbroy102 from isatest; no cygwin test currently running, needs a working server somewhere
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
48209
diff
changeset
|
59 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
60 |
echo "### building distribution" >> $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
61 |
mkdir -p $DISTPREFIX |
49004 | 62 |
"$HOME/hg-isabelle/bin/isabelle" makedist >> $DISTLOG 2>&1 |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
63 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
64 |
if [ $? -ne 0 ] |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
65 |
then |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
66 |
echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
67 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28418
diff
changeset
|
68 |
log "dist build FAILED, elapsed time $ELAPSED." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
69 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
70 |
echo "Could not build isabelle distribution. Log file available at" > $TMP |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
71 |
echo "$HOSTNAME:$DISTLOG" >> $TMP |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
72 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
73 |
for R in $MAILTO; do |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
74 |
$MAIL "isabelle dist build failed" $R $TMP |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
75 |
done |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
76 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
77 |
rm $TMP |
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 |
exit 1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
80 |
fi |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
81 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
82 |
cd $DISTPREFIX >> $DISTLOG 2>&1 |
40739
9c84b562620d
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
wenzelm
parents:
37874
diff
changeset
|
83 |
ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST` |
9c84b562620d
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
wenzelm
parents:
37874
diff
changeset
|
84 |
$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1 |
9c84b562620d
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
wenzelm
parents:
37874
diff
changeset
|
85 |
ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle |
41967
6aa69999da8f
isatest: fresh copy of settings avoids odd cumulative environment;
wenzelm
parents:
41599
diff
changeset
|
86 |
cp Isabelle/etc/settings Isabelle/etc/settings.orig |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
87 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
88 |
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
89 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
90 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
28539
bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents:
28418
diff
changeset
|
91 |
log "dist build successful, elapsed time $ELAPSED." |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
92 |
|
48259 | 93 |
|
22413
3df5c44482e2
clean up var/running dir before spawning new tests
kleing
parents:
22411
diff
changeset
|
94 |
## clean up var/running |
3df5c44482e2
clean up var/running dir before spawning new tests
kleing
parents:
22411
diff
changeset
|
95 |
rm -f $RUNNING/* |
48211
12bbb9d4b6ed
make sure var/running dir exists for isatest
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
48210
diff
changeset
|
96 |
mkdir -p $RUNNING |
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
97 |
|
48259 | 98 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
99 |
## spawn test runs |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
100 |
|
53685 | 101 |
$SSH lxbroy10 "$MAKEALL $HOME/settings/at64-poly" |
53648
924579729403
another move to avoid sporadic kill of poly, which is presumably due to resource management on lxbroy2, lxbroy3 etc.;
wenzelm
parents:
52750
diff
changeset
|
102 |
sleep 15 |
52750 | 103 |
$SSH lxbroy4 " |
48259 | 104 |
$MAKEALL $HOME/settings/at-poly; |
105 |
$MAKEALL $HOME/settings/at-poly-test" |
|
35398
aec00d4ec03d
added at-poly-test, which is intended for performance tests of Poly/ML itself;
wenzelm
parents:
35245
diff
changeset
|
106 |
sleep 15 |
53648
924579729403
another move to avoid sporadic kill of poly, which is presumably due to resource management on lxbroy2, lxbroy3 etc.;
wenzelm
parents:
52750
diff
changeset
|
107 |
$SSH lxbroy3 "$MAKEALL -l HOL-Library $HOME/settings/at-sml-dev-e" |
28598
cb5f98e2e187
give more time to do inital loggin and settings read
kleing
parents:
28539
diff
changeset
|
108 |
sleep 15 |
48209 | 109 |
$SSH macbroy23 "$MAKEALL $HOME/settings/at-poly-e" |
28598
cb5f98e2e187
give more time to do inital loggin and settings read
kleing
parents:
28539
diff
changeset
|
110 |
sleep 15 |
46004
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45913
diff
changeset
|
111 |
$SSH macbroy2 " |
48635 | 112 |
$MAKEALL $HOME/settings/mac-poly64-M4; |
113 |
$MAKEALL $HOME/settings/mac-poly64-M8; |
|
46004
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents:
45913
diff
changeset
|
114 |
$MAKEALL $HOME/settings/mac-poly-M4; |
51562
5fffa75d2432
separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
wenzelm
parents:
49143
diff
changeset
|
115 |
$MAKEALL $HOME/settings/mac-poly-M8; |
53662
396e7db3240c
explicit test of quick_and_dirty, which is rarely used in practice;
wenzelm
parents:
53648
diff
changeset
|
116 |
$MAKEALL $HOME/settings/mac-poly-M8-skip_proofs; |
396e7db3240c
explicit test of quick_and_dirty, which is rarely used in practice;
wenzelm
parents:
53648
diff
changeset
|
117 |
$MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty" |
31581 | 118 |
sleep 15 |
44978 | 119 |
$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2" |
120 |
sleep 15 |
|
49143
ae4fe6e4c3c0
no need to wait 3h on macbroy30 (unlike former macbroy6, cf. 6e5b994070c1);
wenzelm
parents:
49004
diff
changeset
|
121 |
$SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2" |
48210
08cb859c53cd
removed switched-off atbroy102 from isatest; no cygwin test currently running, needs a working server somewhere
Gerwin Klein <gerwin.klein@nicta.com.au>
parents:
48209
diff
changeset
|
122 |
|
22410
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
123 |
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
124 |
|
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
125 |
gzip -f $DISTLOG |
da313b67a04d
moved all isatest/cron job related files to own directory
kleing
parents:
diff
changeset
|
126 |