#!/usr/bin/env bash

#

# $Id$

# Author: Gerwin Klein, TU Muenchen

#

# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.

## global settings

. ~/admin/isatest-settings

TMP=/tmp/isatest-makedist.$$

MAIL=$HOME/bin/pmail

MAKEDIST=$HOME/bin/makedist

MAKEALL=$HOME/bin/isatest-makeall

TAR=gtar

CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK"

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

# cleanup old error log and test-still-running files

rm -f $ERRORLOG

rm -f $ERRORDIR/isatest-*.log

rm -f $RUNNING/*.runnning

export DISTPREFIX

export CVS2CL

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 $HOME/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 ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1

ELAPSED=$("$HOME/bin/showtime" "$SECONDS")

echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG

## spawn test runs

$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly $HOME/settings/sun-sml-dev"

# give test some time to copy settings and start

sleep 5

$SSH atbroy51 "$MAKEALL $HOME/settings/at-poly $HOME/settings/at-sml-dev"

sleep 5

$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly $HOME/settings/mac-sml-dev"

echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1

gzip -f $DISTLOG

## end