Admin/isatest-makedist

use 2 processors on sunbroy1

#!/usr/bin/env bash
#
# $Id$
# Author: Gerwin Klein, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.

# source bashrc, we're called by cron
. ~/.bashrc


## global settings
MAILTO="[e-mail] [e-mail] [e-mail] [e-mail] [e-mail]"

TMP=/tmp/isatest-makedist.$$
MAIL=~/bin/pmail

LOGPREFIX=~/log
MASTERLOG=$LOGPREFIX/isatest.log
DISTPREFIX=~/isadist
MAKEDIST=~/bin/makedist
MAKEALL=~/bin/isatest-makeall
TAR=gtar

SUN=sunbroy2
AT=atbroy51

SSH="ssh -f"

## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG"
  echo
  echo "   Build distribution and run isatest-make for lots of platforms."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

## main

export DISTPREFIX

DATE=$(date "+%Y-%m-%d")
DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log

echo ------------------- preparing test release --- `date` --- $HOSTNAME > $DISTLOG 2>&1

echo "### cleaning up old dist directory"  >> $DISTLOG 2>&1
rm -rf $DISTPREFIX >> $DISTLOG 2>&1

echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1
rm -rf ~/isabelle-*

echo "### building distribution"  >> $DISTLOG 2>&1
$MAKEDIST - >> $DISTLOG 2>&1

if [ $? -ne 0 ]
then
    echo ------------------- DIST BUILD FAILED --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
    echo "$(date) $HOSTNAME $PRG: dist build FAILED, elapsed time $ELAPSED." >> $MASTERLOG

    echo "Could not build isabelle distribution. Log file available at" > $TMP
    echo "$HOSTNAME:$DISTLOG" >> $TMP

    for R in $MAILTO; do
	$MAIL "isabelle dist build failed" $R $TMP
    done

    rm $TMP

    exit 1
fi

cd $DISTPREFIX >> $DISTLOG 2>&1
$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1

echo "### generating development snapshot web page" >> $DISTLOG 2>&1
(cd ~/devel-page; make)

echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
gzip -f $DISTLOG

ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG


## spawn test runs

$SSH sunbroy1 "$MAKEALL $DISTPREFIX ~/settings/sun1-poly ~/settings/sun1-sml"
$SSH $SUN "$MAKEALL $DISTPREFIX ~/settings/sun-poly ~/settings/sun-sml"
$SSH $AT "$MAKEALL $DISTPREFIX ~/settings/at-poly ~/settings/at-sml"

## end