| author | blanchet | 
| Mon, 16 Dec 2013 09:48:26 +0100 | |
| changeset 54764 | 1c9ef5c834e8 | 
| 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: 
48209diff
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: 
28418diff
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: 
37874diff
changeset | 83 | ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST` | 
| 
9c84b562620d
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
 wenzelm parents: 
37874diff
changeset | 84 | $TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1 | 
| 
9c84b562620d
recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
 wenzelm parents: 
37874diff
changeset | 85 | ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle | 
| 41967 
6aa69999da8f
isatest: fresh copy of settings avoids odd cumulative environment;
 wenzelm parents: 
41599diff
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: 
28418diff
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: 
22411diff
changeset | 94 | ## clean up var/running | 
| 
3df5c44482e2
clean up var/running dir before spawning new tests
 kleing parents: 
22411diff
changeset | 95 | rm -f $RUNNING/* | 
| 48211 
12bbb9d4b6ed
make sure var/running dir exists for isatest
 Gerwin Klein <gerwin.klein@nicta.com.au> parents: 
48210diff
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: 
52750diff
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: 
35245diff
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: 
52750diff
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: 
28539diff
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: 
28539diff
changeset | 110 | sleep 15 | 
| 46004 
484ef66bc3a1
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
 wenzelm parents: 
45913diff
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: 
45913diff
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: 
49143diff
changeset | 115 | $MAKEALL $HOME/settings/mac-poly-M8; | 
| 53662 
396e7db3240c
explicit test of quick_and_dirty, which is rarely used in practice;
 wenzelm parents: 
53648diff
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: 
53648diff
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: 
49004diff
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: 
48209diff
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 |