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: Build distribution and run isatest-make for lots of platforms.
|
|
8 |
|
13237
|
9 |
# source bashrc, we're called by cron
|
|
10 |
. ~/.bashrc
|
|
11 |
|
|
12 |
|
13231
|
13 |
## global settings
|
13246
|
14 |
MAILTO="kleing@in.tum.de test@jflex.de"
|
|
15 |
|
13233
|
16 |
LOGPREFIX=~/log
|
13237
|
17 |
MASTERLOG=$LOGPREFIX/isatest.log
|
13231
|
18 |
DISTPREFIX=~/isadist
|
|
19 |
MAKEDIST=~/bin/makedist
|
13234
|
20 |
MAKEALL=~/bin/isatest-makeall
|
|
21 |
TAR=gtar
|
13231
|
22 |
|
|
23 |
SUN=sunbroy2
|
|
24 |
AT=atbroy37
|
|
25 |
|
13233
|
26 |
SSH="ssh -f"
|
13231
|
27 |
|
|
28 |
## diagnostics
|
|
29 |
|
|
30 |
PRG="$(basename "$0")"
|
|
31 |
|
|
32 |
function usage()
|
|
33 |
{
|
|
34 |
echo
|
|
35 |
echo "Usage: $PRG"
|
|
36 |
echo
|
|
37 |
echo " Build distribution and run isatest-make for lots of platforms."
|
|
38 |
echo
|
|
39 |
exit 1
|
|
40 |
}
|
|
41 |
|
|
42 |
function fail()
|
|
43 |
{
|
|
44 |
echo "$1" >&2
|
|
45 |
exit 2
|
|
46 |
}
|
|
47 |
|
|
48 |
## main
|
|
49 |
|
|
50 |
export DISTPREFIX
|
|
51 |
|
|
52 |
DATE=$(date "+%d-%b-%Y")
|
|
53 |
DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
|
|
54 |
|
|
55 |
echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
|
|
56 |
|
|
57 |
echo "### cleaning up old dist directory" >> $DISTLOG 2>&1
|
|
58 |
rm -rf $DISTPREFIX >> $DISTLOG 2>&1
|
|
59 |
|
13237
|
60 |
echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
|
|
61 |
rm -rf ~/isabelle-*
|
|
62 |
|
13231
|
63 |
echo "### building distribution" >> $DISTLOG 2>&1
|
|
64 |
$MAKEDIST - >> $DISTLOG 2>&1
|
|
65 |
|
|
66 |
if [ $? -ne 0 ]
|
|
67 |
then
|
|
68 |
echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
|
13237
|
69 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
|
|
70 |
echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
|
13246
|
71 |
|
|
72 |
for R in $MAILTO; do
|
|
73 |
mail -t $R <<EOM
|
|
74 |
Subject: isabelle dist build failed
|
|
75 |
|
|
76 |
Could not build isabelle distribution. Log file available at
|
|
77 |
|
|
78 |
$HOSTNAME:$DISTLOG
|
|
79 |
EOM
|
|
80 |
done
|
|
81 |
|
13231
|
82 |
# more action here
|
|
83 |
exit 1
|
|
84 |
fi
|
|
85 |
|
|
86 |
cd $DISTPREFIX >> $DISTLOG 2>&1
|
13234
|
87 |
$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
|
13231
|
88 |
|
|
89 |
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
|
13237
|
90 |
gzip -f $DISTLOG
|
|
91 |
|
|
92 |
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
|
|
93 |
echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
|
|
94 |
|
13231
|
95 |
|
|
96 |
## spawn test runs
|
|
97 |
|
|
98 |
# run tests in parallel on multiprocessor sun
|
13246
|
99 |
$SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly ~/settings/sun-sml"
|
|
100 |
# $SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-sml"
|
13231
|
101 |
|
|
102 |
# run tests sequentially on x86
|
13234
|
103 |
$SSH $AT "$MAKEALL $DISTPREFIX ~/settings/at-poly ~/settings/at-sml"
|
13231
|
104 |
|
13234
|
105 |
## end
|