Admin/isatest-makedist
author berghofe
Mon, 05 Aug 2002 14:35:33 +0200
changeset 13455 f88a91ff8ac6
parent 13431 b0ba3b3573e1
child 13680 a6ce43a59d4a
permissions -rwxr-xr-x
Removed theory NatDef.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     1
#!/usr/bin/env bash
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     2
#
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     3
# $Id$
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     4
# Author: Gerwin Klein, TU Muenchen
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     5
# License: GPL (GNU GENERAL PUBLIC LICENSE)
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     6
#
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     7
# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
     8
13237
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
     9
# source bashrc, we're called by cron
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    10
. ~/.bashrc
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    11
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    12
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    13
## global settings
13359
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    14
MAILTO="kleing@in.tum.de nipkow@in.tum.de wenzelm@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk"
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    15
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    16
TMP=/tmp/isatest-makedist.$$
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    17
MAIL=~/bin/pmail
13246
e51efc2029e9 email sending
isatest
parents: 13237
diff changeset
    18
13233
kleing
parents: 13231
diff changeset
    19
LOGPREFIX=~/log
13237
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    20
MASTERLOG=$LOGPREFIX/isatest.log
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    21
DISTPREFIX=~/isadist
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    22
MAKEDIST=~/bin/makedist
13234
isatest
parents: 13233
diff changeset
    23
MAKEALL=~/bin/isatest-makeall
isatest
parents: 13233
diff changeset
    24
TAR=gtar
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    25
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    26
SUN=sunbroy2
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    27
AT=atbroy37
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    28
13233
kleing
parents: 13231
diff changeset
    29
SSH="ssh -f"
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    30
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    31
## diagnostics
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    32
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    33
PRG="$(basename "$0")"
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    34
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    35
function usage()
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    36
{
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    37
  echo
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    38
  echo "Usage: $PRG"
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    39
  echo
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    40
  echo "   Build distribution and run isatest-make for lots of platforms."
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    41
  echo
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    42
  exit 1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    43
}
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    44
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    45
function fail()
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    46
{
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    47
  echo "$1" >&2
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    48
  exit 2
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    49
}
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    50
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    51
## main
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    52
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    53
export DISTPREFIX
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    54
13431
b0ba3b3573e1 changed date format for proper lexicographical ordering
isatest
parents: 13359
diff changeset
    55
DATE=$(date "+%Y-%m-%d")
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    56
DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    57
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    58
echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    59
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    60
echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    61
rm -rf $DISTPREFIX >> $DISTLOG 2>&1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    62
13237
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    63
echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    64
rm -rf ~/isabelle-*
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    65
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    66
echo "### building distribution"  >> $DISTLOG 2>&1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    67
$MAKEDIST - >> $DISTLOG 2>&1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    68
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    69
if [ $? -ne 0 ]
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    70
then
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    71
    echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
13237
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    72
    ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    73
    echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG
13246
e51efc2029e9 email sending
isatest
parents: 13237
diff changeset
    74
13359
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    75
    echo "Could not build isabelle distribution. Log file available at" > $TMP
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    76
    echo "$HOSTNAME:$DISTLOG" >> $TMP
13246
e51efc2029e9 email sending
isatest
parents: 13237
diff changeset
    77
13359
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    78
    for R in $MAILTO; do
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    79
	$MAIL "isabelle dist build failed" $R $TMP
13246
e51efc2029e9 email sending
isatest
parents: 13237
diff changeset
    80
    done
e51efc2029e9 email sending
isatest
parents: 13237
diff changeset
    81
13359
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    82
    rm $TMP
982827aacb39 mail address update
isatest
parents: 13246
diff changeset
    83
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    84
    exit 1
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    85
fi
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    86
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    87
cd $DISTPREFIX >> $DISTLOG 2>&1
13234
isatest
parents: 13233
diff changeset
    88
$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    89
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    90
echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
13237
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    91
gzip -f $DISTLOG
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    92
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    93
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    94
echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
493d61afa731 cleanup old isabelle-* dirs before test start
isatest
parents: 13234
diff changeset
    95
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    96
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    97
## spawn test runs
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    98
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
    99
# run tests in parallel on multiprocessor sun 
13246
e51efc2029e9 email sending
isatest
parents: 13237
diff changeset
   100
$SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly ~/settings/sun-sml"
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   101
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   102
# run tests sequentially on x86
13234
isatest
parents: 13233
diff changeset
   103
$SSH $AT "$MAKEALL $DISTPREFIX ~/settings/at-poly ~/settings/at-sml"
13231
cce28efb2600 for nightly test builds
kleing
parents:
diff changeset
   104
13234
isatest
parents: 13233
diff changeset
   105
## end