Admin/isatest/isatest-makedist
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 56997 ab28906b54ae
child 58471 ab4b94892c4c
permissions -rwxr-xr-x
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
3a324a3f4aea more formal isabelle makedist from repository;
wenzelm
parents: 48832
diff changeset
     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
654bf12de98b switch from gtar to tar
isatest
parents: 26727
diff changeset
    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
56997
ab28906b54ae more explicit identification for more robust adhoc change of environment /home/isatest/.isabelle/etc/settings -- notably for $ISABELLE_PLATFORM64;
wenzelm
parents: 53685
diff changeset
    18
export THIS_IS_ISATEST_MAKEDIST=true
ab28906b54ae more explicit identification for more robust adhoc change of environment /home/isatest/.isabelle/etc/settings -- notably for $ISABELLE_PLATFORM64;
wenzelm
parents: 53685
diff changeset
    19
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    20
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    21
## diagnostics
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
PRG="$(basename "$0")"
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
function usage()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    26
{
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 "Usage: $PRG"
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
  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
    31
  echo
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    32
  exit 1
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
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    35
function fail()
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    36
{
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    37
  echo "$1" >&2
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    38
  exit 2
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    39
}
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    40
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    41
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    42
## main
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
# cleanup old error log and test-still-running files
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    45
rm -f $ERRORLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    46
rm -f $ERRORDIR/isatest-*.log
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    47
rm -f $RUNNING/*.runnning
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
export DISTPREFIX
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    50
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    51
DATE=$(date "+%Y-%m-%d")
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    52
DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
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 ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    55
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    56
echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    57
rm -rf $DISTPREFIX >> $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    58
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    59
echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    60
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
    61
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    62
echo "### building distribution"  >> $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    63
mkdir -p $DISTPREFIX
49004
3a324a3f4aea more formal isabelle makedist from repository;
wenzelm
parents: 48832
diff changeset
    64
"$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
    65
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    66
if [ $? -ne 0 ]
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    67
then
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    68
    echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    69
    ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28418
diff changeset
    70
    log "dist build FAILED, elapsed time $ELAPSED."
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    71
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    72
    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
    73
    echo "$HOSTNAME:$DISTLOG" >> $TMP
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    74
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    75
    for R in $MAILTO; do
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    76
        $MAIL "isabelle dist build failed" $R $TMP
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    77
    done
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
    rm $TMP
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    80
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    81
    exit 1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    82
fi
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    83
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    84
cd $DISTPREFIX >> $DISTLOG 2>&1
40739
9c84b562620d recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
wenzelm
parents: 37874
diff changeset
    85
ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST`
9c84b562620d recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
wenzelm
parents: 37874
diff changeset
    86
$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1
9c84b562620d recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce);
wenzelm
parents: 37874
diff changeset
    87
ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle
41967
6aa69999da8f isatest: fresh copy of settings avoids odd cumulative environment;
wenzelm
parents: 41599
diff changeset
    88
cp Isabelle/etc/settings Isabelle/etc/settings.orig
22410
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
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    91
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    92
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
28539
bdb308737bfd do logging to MASTERLOG centrally (avoid multiple writers over NFS as
kleing
parents: 28418
diff changeset
    93
log "dist build successful, elapsed time $ELAPSED."
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    94
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
    95
22413
3df5c44482e2 clean up var/running dir before spawning new tests
kleing
parents: 22411
diff changeset
    96
## clean up var/running
3df5c44482e2 clean up var/running dir before spawning new tests
kleing
parents: 22411
diff changeset
    97
rm -f $RUNNING/*
48211
12bbb9d4b6ed make sure var/running dir exists for isatest
Gerwin Klein <gerwin.klein@nicta.com.au>
parents: 48210
diff changeset
    98
mkdir -p $RUNNING
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
    99
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   100
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   101
## spawn test runs
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   102
53685
983711bc98e0 actually use x86_64 machine;
wenzelm
parents: 53662
diff changeset
   103
$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
   104
sleep 15
52750
96d53ab825cf avoid machine running batch process for months;
wenzelm
parents: 51562
diff changeset
   105
$SSH lxbroy4 "
48259
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   106
  $MAKEALL $HOME/settings/at-poly;
1635298d8fe7 removed some old/unused stuff;
wenzelm
parents: 48258
diff changeset
   107
  $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
   108
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
   109
$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
   110
sleep 15
48209
67f13db5d273 prefer lxbroy[23] as standard test machines;
wenzelm
parents: 48158
diff changeset
   111
$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
   112
sleep 15
46004
484ef66bc3a1 more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
wenzelm
parents: 45913
diff changeset
   113
$SSH macbroy2 "
48635
bfce940c6f38 clarified ISABELLE_FULL_TEST;
wenzelm
parents: 48608
diff changeset
   114
  $MAKEALL $HOME/settings/mac-poly64-M4;
bfce940c6f38 clarified ISABELLE_FULL_TEST;
wenzelm
parents: 48608
diff changeset
   115
  $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
   116
  $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
   117
  $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
   118
  $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
   119
  $MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty"
31581
907616b9536c more isatests;
wenzelm
parents: 31385
diff changeset
   120
sleep 15
44978
a04f3eb3943c isatest settings for macbroy6 (Mac OS X Lion);
wenzelm
parents: 43506
diff changeset
   121
$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
a04f3eb3943c isatest settings for macbroy6 (Mac OS X Lion);
wenzelm
parents: 43506
diff changeset
   122
sleep 15
49143
ae4fe6e4c3c0 no need to wait 3h on macbroy30 (unlike former macbroy6, cf. 6e5b994070c1);
wenzelm
parents: 49004
diff changeset
   123
$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
   124
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   125
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   126
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   127
gzip -f $DISTLOG
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset
   128