Work at SourceForge, help us to make it a better place! We have an immediate need for a Support Technician in our San Francisco or Denver office.

Close

[69143c]: admin / testall Maximize Restore History

Download this file

testall    114 lines (98 with data), 2.7 kB

#!/usr/bin/env bash
#
# $Id: testall,v 1.1.2.4 2004-03-19 00:20:38 lsf37 Exp $
# Author: Gerwin Klein, NICTA
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# Tests all entries in Archive of Formal Proofs
# 

## settings

function usage()
{
  echo
  echo "Usage: $PRG OPTIONS [entries]"
  echo
  echo "  Runs isatool make on specified entries in the Archive of Formal Proofs"
  echo 
  echo "Options:"
  echo "-t <path/to/isatool>   use isatool at specified path"     
  echo "-c                     include target clean (rebuild session)"
  echo "-d <path>              use specified path as base for archive entries"
  echo "-r                     use env variable ISABELLE_RELEASES to find isatool"
  echo 
  echo "Examples:"
  echo
  echo "$PRG"
  echo   "uses isatool in your normal path to run all tests (usually = devel version)"
  echo
  echo "$PRG Example-Submission"
  echo   "same as above, but only test Example-Submission"
  echo
  echo "$PRG -t /usr/proj/isabelle/Isabelle2003/bin/isatool Example-Submission"
  echo   "uses the Isabelle 2003 release version to run the test"
  echo
  echo "$PRG -r Isabelle2003 Example-Submission"
  echo   "uses the distribution $ISABELLE_RELEASES/Isabelle2003 to test Example-Submission"
  exit 1
}

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

function check_isatool()
{
  [ -x $ISATOOL ] || fail "No isatool found at [$ISATOOL]."
  ML_IDENTIFIER=`$ISATOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
  ISABELLE_HOME=`$ISATOOL getenv -b ISABELLE_HOME` || fail "could not find Isabelle home"
  [ -n "$ISABELLE_IMAGE_PATH" ] || export ISABELLE_IMAGE_PATH="$ISABELLE_HOME/heaps/$ML_IDENTIFIER/"
}

## 

PRG="$(basename "$0")"
THYS="$(dirname "$0")/../thys"

[ "$1" = "-?" ] && usage

ISATOOL=isatool
while getopts "t:cr:d:" OPT
do
    case "$OPT" in
      r)
        [ "$ISABELLE_RELEASES" == "" ] && fail "ISABELLE_RELEASES not set"
        ISATOOL="$ISABELLE_RELEASES/$OPTARG/bin/isatool"
        check_isatool
        ;;
      c)
        CLEAN="clean"
        ;;
      d)
        THYS="$OPTARG"
        ;;
      t)
        ISATOOL="$OPTARG"
        check_isatool
        ;;
    esac
done

shift $(($OPTIND - 1))

[ -d $THYS ] || fail "Could not find archive directory. Tried [$THYS]."
cd $THYS

DIRS=$@
if [ "$DIRS" == "" ]; then DIRS=*; fi

FAIL="";

for DIR in $DIRS; do
    if [ -d $DIR -a "$DIR" != "CVS" ]; then
        echo "Testing [$DIR]"
        cd $DIR
        $ISATOOL make $CLEAN all $@ || FAIL="${FAIL}${DIR} "
        cd ..
        echo "Finished [$DIR]"
    fi
done

if [ "$FAIL" != "" ]; then 
    echo "The following tests failed:"
    echo "$FAIL"
    echo "Please check logs."
    exit 1
else
    echo "All tests successful."
    exit 0
fi