#!/usr/bin/env bash
#
# $Id$
# Author: Gerwin Klein, TU Muenchen
#
# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.
# source bashrc, we're called by cron
. ~/.bashrc
# canoncical home for all platforms
HOME=/usr/stud/isatest
## global settings
MAILTO="kleing@in.tum.de nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk skalberg@in.tum.de"
TMP=/tmp/isatest-makedist.$$
MAIL=$HOME/bin/pmail
LOGPREFIX=$HOME/log
MASTERLOG=$LOGPREFIX/isatest.log
ERRORDIR=$HOME/var
ERRORLOG=$ERRORDIR/error.log
RUNNING=$HOME/var/running
DISTPREFIX=$HOME/tmp/isadist
MAKEDIST=$HOME/bin/makedist
MAKEALL=$HOME/bin/isatest-makeall
TAR=gtar
CVS2CL=$HOME/bin/cvs2cl
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
gzip -f $DISTLOG
ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG
## spawn test runs
$SSH sunbroy2 "$MAKEALL $DISTPREFIX $HOME/settings/sun-poly $HOME/settings/sun-sml $HOME/settings/sun-sml-dev"
# give test some time to copy settings and start
sleep 5
$SSH atbroy51 "$MAKEALL $DISTPREFIX $HOME/settings/at-poly $HOME/settings/at-sml"
# wakeup call for macbroy33
wakeonlan -i 131.159.47.255 00:30:65:DA:35:E0 > /dev/null
sleep 5
$SSH macbroy33 "$MAKEALL $DISTPREFIX $HOME/settings/mac-poly"
## end