[7ea318]: admin / regression  Maximize  Restore  History

Download this file

194 lines (146 with data), 4.8 kB

#!/usr/bin/env bash
#
# Author: Gerwin Klein, NICTA
#
# Automated regression test to be run from cron.
# Sends email to maintainers if test fails.
#
# Relies on being run in the isatest environment.
# 

. ~/.bashrc

## settings

ISABELLE_RELEASES=${ISABELLE_RELEASES:-/home/isabelle}
WORKING_COPY=~/afp

HOST="$(hostname -s)"

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

TMP=`mktemp -q /tmp/afp-regression.mail.XXXXXX` \
 || fail "could not make tmp file"

#

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

## functions

function usage()
{
  echo
  echo "Usage: $PRG [-f] [-|release_tag]"
  echo
  echo "  Runs testall from cron and logs output"
  echo
  echo "Options: -f   only run test that are marked as frequent"
  echo 
  exit 1
}

## 

if [ "$1" == "-f" ]; then
	FRQ="-f"
	shift
fi

[ "$#" != "1" -o "$1" = "-?" ] && usage

if [ "$1" == "-" ]; then
  AFP_VER="development"
  WORKING_COPY=$WORKING_COPY/devel

  . $WORKING_COPY/admin/main-config || fail "could not read main-config."

  "$DIR/prepare-release" || fail "could not prepare Isabelle snapshot."

  ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isabelle

  ML_IDENTIFIER=`$ISABELLE_TOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
  ISABELLE_HOME_USER=`$ISABELLE_TOOL getenv -b ISABELLE_HOME_USER` || fail "could not identify ISABELLE_HOME_USER"
  export ISABELLE_IMAGE_PATH="$ISABELLE_HOME_USER/heaps/$ML_IDENTIFIER/"
  
  LOG=$LOG-devel-$DATE.log
  SNAPSHOT=1;
  REPORT=$REPORT-devel

  BROWSER_INFO=`$ISABELLE_TOOL getenv -b ISABELLE_BROWSER_INFO` || fail "could not find browser info"
  [ -e "$BROWSER_INFO" ] && rm -rf $BROWSER_INFO

  ISABELLE_HG_ID="$(cat $ISABELLE_IDENT)"
  ISABELLE_DATE=$DATE
  ISABELLE_VER="devel -- hg id $ISABELLE_HG_ID"
else
  AFP_VER="release ($1)"
  WORKING_COPY=$WORKING_COPY/release

  . $WORKING_COPY/admin/main-config || fail "could not read main-config."

  ISABELLE_TOOL=$ISABELLE_RELEASES/$1/bin/isabelle
  ML_IDENTIFIER=`$ISABELLE_TOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
  export ISABELLE_IMAGE_PATH="$ISABELLE_RELEASES/$1/heaps/$ML_IDENTIFIER/"
  LOG=$LOG-$1-$DATE.log
  REPORT=$REPORT-$1
  
  ISABELLE_VER="release -- $($ISABELLE_TOOL version)"
fi

MAIL="$WORKING_COPY/admin/mail-attach"

echo "Start test for $WORKING_COPY at `date`, $HOST" > $LOG
echo >> $LOG
echo "begin hg pull/update" >> $LOG

# hg pull -u to newest version of archive 
cd $WORKING_COPY || fail "could not cd to $WORKING_COPY"
hg pull -u >> $LOG 2>&1 || fail "could not hg pull."

echo "end hg pull/update" >> $LOG
echo >> $LOG

AFP_HG_ID="$(hg id -i)"
AFP_HG_ID="${AFP_HG_ID%+}"
AFP_DATE="$(hg log -l 1 -r $AFP_HG_ID --template '{date|isodate}')"
AFP_VERSION="AFP version: $AFP_VER -- hg id $AFP_HG_ID"
ISA_VERSION="Isabelle version: $ISABELLE_VER"

echo "$AFP_VERSION" >> $LOG
echo "$ISA_VERSION" >> $LOG
echo >> $LOG

# run test
$WORKING_COPY/admin/testall $FRQ -t $ISABELLE_TOOL -c >> $LOG 2>&1
FAILURE=$?

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

echo >> $LOG
echo "End test on `date`, $HOST, elapsed time: $ELAPSED" >> $LOG

# generate report
DIFF=`$WORKING_COPY/admin/report.pl $LOG $REPORT`

# send mail on status changes
if [ -n "$DIFF" ]; then
  cat > $TMP <<EOF
The status of the following AFP entries changed or remains FAIL: 
$DIFF

Full entry status at http://afp.sourceforge.net/status.shtml

$AFP_VERSION
$ISA_VERSION
Test ended on: $HOST, `date`.

Have a nice day,
  isatest

EOF
  for R in $MAIN_NOTIFY; do
    $MAIL 'status (AFP)' "$R" $TMP $REPORT $LOG
  done  
fi

# send email to maintainer if there was a problem
if [ "$FAILURE" != "0" ]; then
  FAIL=`tail -4 $LOG | head -1`
  echo "`date`, $HOST, $AFP_VER [afp: $AFP_HG_ID, isa: $ISABELLE_VER]: test failed on [$FAIL]. Elapsed time: $ELAPSED" >> $MASTERLOG
  for E in $FAIL; do
    (
      . $WORKING_COPY/thys/$E/config || fail "error reading config for $E"
      if [ "$FREQUENT" == "yes" ]; then
        cat > $TMP <<EOF
Session [$E] in the automated afp test failed. 

$AFP_VERSION
$ISA_VERSION
Test ended on: $HOST, `date`.

To reproduce the error, check out the $AFP_VER version of the
archive from sourceforge and run "isabelle make" on your session.

This is an automatically generated email. To switch off these 
notifications, edit thys/$E/config and hg commit and push the changes.

Have a nice day,
  isatest

EOF
        for R in $NOTIFY; do
          $MAIL 'test failed (Archive of Formal Proofs)' "$R" $TMP $LOG
        done
      fi
    )
  done
else
  echo "`date`, $HOST, $AFP_VER [afp: $AFP_HG_ID, isa: $ISABELLE_VER]: All tests successful. Elapsed time: $ELAPSED" >> $MASTERLOG
fi

# clean up tmp
rm -f $TMP

# make devel snapshot
if [ "$SNAPSHOT" == "1" ]; then
    $WORKING_COPY/admin/make-web-devel "$BROWSER_INFO" $ISABELLE_HG_ID "$ISABELLE_DATE" $AFP_HG_ID "$AFP_DATE" || fail "failed to prepare snapshot"
fi

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

JavaScript is required for this form.





No, thanks