lib/Tools/usedir

simpler proofs of congruence rules

#!/bin/bash
#
# $Id$
#
# DESCRIPTION: build object-logic or run examples


## diagnostics

PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG LOGIC NAME"
  echo
  echo "  Options are:"
  echo "    -b           build mode (output heap image, using current dir)"
  echo "    -i BOOL      generate theory browsing information,"
  echo "                 i.e. HTML / graph data (default false)"
  echo "    -r           reset session path"
  echo "    -s NAME      override session NAME"
  echo
  echo "  Build object-logic or run examples. Also creates browsing"
  echo "  information (HTML etc.) according to settings."
  echo
  exit 1
}


## process command line

# options

BUILD=""
INFO=false
RESET=false
SESSION=""

function getoptions()
{
  OPTIND=1
  while getopts "bi:rs:" OPT
  do
    case "$OPT" in
      b)
        BUILD=true
        ;;
      i)
        INFO="$OPTARG"
        ;;
      r)
        RESET=true
        ;;
      s)
        SESSION="$OPTARG"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

getoptions $ISABELLE_USEDIR_OPTIONS

getoptions "$@"
shift $(($OPTIND - 1))


# args

[ $# -ne 2 ] && usage

LOGIC="$1"; shift
NAME="$1"; shift

[ -z "$SESSION" ] && SESSION=$(basename $NAME)



## main

# prepare browser info dir

if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then

  mkdir -p $ISABELLE_BROWSER_INFO/gif
  cp $ISABELLE_HOME/lib/images/blue_arrow.gif $ISABELLE_BROWSER_INFO/gif
  cp $ISABELLE_HOME/lib/images/red_arrow.gif $ISABELLE_BROWSER_INFO/gif
  cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/gif/isabelle.gif
  cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html

  mkdir -p $ISABELLE_BROWSER_INFO/graph
  cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
  mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
  mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
  cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
  cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities

fi


# prepare log dir

LOGDIR="$ISABELLE_OUTPUT/log"
mkdir -p "$LOGDIR"


# run isabelle

SECONDS=0

PARENT=$(basename "$LOGIC")

if [ -n "$BUILD" ]; then
  ITEM="$SESSION"
  echo -n "Building $ITEM ... "
  LOG="$LOGDIR/$ITEM"

  $ISABELLE \
    -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\";" \
    -q -w $LOGIC $NAME > $LOG 2>&1
  RC=$?
else
  ITEM=$(basename $LOGIC)-"$SESSION"
  echo -n "Running $ITEM ... "
  LOG="$LOGDIR/$ITEM"

  cd "$NAME"
  $ISABELLE \
    -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\"; quit();" \
    -r -q $LOGIC > $LOG 2>&1
  RC=$?
  cd ..
fi

ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)


# exit status

if [ $RC -eq 0 ]; then
  echo "OK  ($ELAPSED elapsed time)"
  gzip --force "$LOG"
else
  echo "FAILED"
  echo "(see also $LOG)"
  echo; tail $LOG; echo
fi

exit $RC