1 #!/usr/bin/env bash |
|
2 # |
|
3 # Author: Gerwin Klein, TU Muenchen |
|
4 # |
|
5 # DESCRIPTION: Build distribution and run isatest-make for lots of platforms. |
|
6 |
|
7 ## global settings |
|
8 . "$HOME/hg-isabelle/Admin/isatest/isatest-settings" |
|
9 |
|
10 TMP=/tmp/isatest-makedist.$$ |
|
11 MAIL=$HOME/bin/pmail |
|
12 |
|
13 MAKEALL=$HOME/bin/isatest-makeall |
|
14 TAR=tar |
|
15 |
|
16 SSH="ssh -f" |
|
17 |
|
18 export THIS_IS_ISATEST_MAKEDIST=true |
|
19 |
|
20 |
|
21 ## diagnostics |
|
22 |
|
23 PRG="$(basename "$0")" |
|
24 |
|
25 function usage() |
|
26 { |
|
27 echo |
|
28 echo "Usage: $PRG" |
|
29 echo |
|
30 echo " Build distribution and run isatest-make for lots of platforms." |
|
31 echo |
|
32 exit 1 |
|
33 } |
|
34 |
|
35 function fail() |
|
36 { |
|
37 echo "$1" >&2 |
|
38 exit 2 |
|
39 } |
|
40 |
|
41 |
|
42 ## main |
|
43 |
|
44 # cleanup old error log and test-still-running files |
|
45 rm -f $ERRORLOG |
|
46 rm -f $ERRORDIR/isatest-*.log |
|
47 rm -f $RUNNING/*.runnning |
|
48 |
|
49 export DISTPREFIX |
|
50 |
|
51 DATE=$(date "+%Y-%m-%d") |
|
52 DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log |
|
53 |
|
54 echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1 |
|
55 |
|
56 echo "### cleaning up old dist directory" >> $DISTLOG 2>&1 |
|
57 rm -rf $DISTPREFIX >> $DISTLOG 2>&1 |
|
58 |
|
59 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1 |
|
60 rm -rf $HOME/isabelle-* |
|
61 |
|
62 echo "### building distribution" >> $DISTLOG 2>&1 |
|
63 mkdir -p $DISTPREFIX |
|
64 "$HOME/hg-isabelle/bin/isabelle" makedist >> $DISTLOG 2>&1 |
|
65 |
|
66 if [ $? -ne 0 ] |
|
67 then |
|
68 echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
|
69 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
|
70 log "dist build FAILED, elapsed time $ELAPSED." |
|
71 |
|
72 echo "Could not build isabelle distribution. Log file available at" > $TMP |
|
73 echo "$HOSTNAME:$DISTLOG" >> $TMP |
|
74 |
|
75 for R in $MAILTO; do |
|
76 $MAIL "isabelle dist build failed" $R $TMP |
|
77 done |
|
78 |
|
79 rm $TMP |
|
80 |
|
81 exit 1 |
|
82 fi |
|
83 |
|
84 cd $DISTPREFIX >> $DISTLOG 2>&1 |
|
85 ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST` |
|
86 $TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1 |
|
87 ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle |
|
88 cp Isabelle/etc/settings Isabelle/etc/settings.orig |
|
89 |
|
90 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
|
91 |
|
92 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
|
93 log "dist build successful, elapsed time $ELAPSED." |
|
94 |
|
95 |
|
96 ## clean up var/running |
|
97 rm -f $RUNNING/* |
|
98 mkdir -p $RUNNING |
|
99 |
|
100 |
|
101 ## spawn test runs |
|
102 |
|
103 $SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly" |
|
104 sleep 15 |
|
105 $SSH lxbroy4 "$MAKEALL -l HOL-Library $HOME/settings/at-poly" |
|
106 sleep 15 |
|
107 $SSH macbroy2 " |
|
108 $MAKEALL $HOME/settings/mac-poly64-M4; |
|
109 $MAKEALL $HOME/settings/mac-poly64-M8; |
|
110 $MAKEALL $HOME/settings/mac-poly-M4; |
|
111 $MAKEALL $HOME/settings/mac-poly-M8; |
|
112 $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs; |
|
113 $MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty" |
|
114 sleep 15 |
|
115 $SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2" |
|
116 sleep 15 |
|
117 $SSH macbroy31 "$MAKEALL $HOME/settings/mac-poly64-M2" |
|
118 |
|
119 echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
|
120 |
|
121 gzip -f $DISTLOG |
|
122 |
|