Admin/isatest/isatest-makedist

tuned proof - no smt call

#!/usr/bin/env bash
#
# Author: Gerwin Klein, TU Muenchen
#
# DESCRIPTION: Build distribution and run isatest-make for lots of platforms.

## global settings
. ~/admin/isatest/isatest-settings

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

MAKEDIST=$HOME/bin/makedist
MAKEALL=$HOME/bin/isatest-makeall
TAR=tar

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

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-*
ssh atbroy102 "rm -rf /home/isatest/isabelle-cygwin-poly-e"

echo "### building distribution"  >> $DISTLOG 2>&1
mkdir -p $DISTPREFIX
$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120313" >> $DISTLOG 2>&1

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

    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
ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST`
$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1
ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle
cp Isabelle/etc/settings Isabelle/etc/settings.orig

ssh atbroy102 "rm -rf /home/isatest/isadist && mkdir -p /home/isatest/isadist" && \
rsync -a "$HOME/isadist/." atbroy102:/home/isatest/isadist/.

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

ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
log "dist build successful, elapsed time $ELAPSED."

## clean up var/running
rm -f $RUNNING/*

## spawn test runs

$SSH macbroy21 "$MAKEALL $HOME/settings/at-poly-test"
# give test some time to copy settings and start
sleep 15
$SSH macbroy28 "$MAKEALL $HOME/settings/at-poly; $MAKEALL $HOME/settings/at-poly-e"
sleep 15
$SSH macbroy22 "$MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
sleep 15
$SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
$SSH macbroy2 "
  $MAKEALL -l . full $HOME/settings/mac-poly64-M4;
  $MAKEALL -l . full $HOME/settings/mac-poly64-M8;
  $MAKEALL $HOME/settings/mac-poly-M4;
  $MAKEALL $HOME/settings/mac-poly-M8"
sleep 15
$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
sleep 15
$SSH macbroy30 "sleep 10800; $MAKEALL $HOME/settings/mac-poly-M2"
sleep 15
$SSH atbroy102 "$MAKEALL $HOME/settings/cygwin-poly-e"
#sleep 15
#$SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"

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

gzip -f $DISTLOG

## end