lib/Tools/usedir

Fixed proof term bug in permute_prems.

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: build object-logic or run examples


## diagnostics

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

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] LOGIC NAME"
  echo
  echo "  Options are:"
  echo "    -D PATH      dump generated document sources into PATH"
  echo "    -P PATH      set path for remote theory browsing information"
  echo "    -b           build mode (output heap image, using current dir)"
  echo "    -c BOOL      tell ML system to compress output image (default true)"
  echo "    -d FORMAT    build document as FORMAT (default false)"
  echo "    -i BOOL      generate theory browser information (default false)"
  echo "    -m MODE      add print mode for output"
  echo "    -p LEVEL     set level of detail for proof objects"
  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
  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
  echo
  exit 1
}


## process command line

# options

DUMP=""
RPATH=""
BUILD=""
COMPRESS=true
DOCUMENT=false
INFO=false
MODES=""
RESET=false
SESSION=""
PROOFS=0

function getoptions()
{
  OPTIND=1
  while getopts "D:P:bc:d:i:m:p:rs:" OPT
  do
    case "$OPT" in
      D)
        DUMP="$OPTARG"
        ;;
      P)
        RPATH="$OPTARG"
        ;;
      b)
        BUILD=true
        ;;
      c)
        COMPRESS="$OPTARG"
        ;;
      d)
        DOCUMENT="$OPTARG"
        ;;
      i)
        INFO="$OPTARG"
        ;;
      m)
        if [ -z "$MODES" ]; then
          MODES="\"$OPTARG\""
        else
          MODES="\"$OPTARG\", $MODES"
        fi
        ;;
      p)
        PROOFS="$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"
  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
  cp "$ISABELLE_HOME/lib/html/index.html" "$ISABELLE_BROWSER_INFO/index.html"
fi


# prepare log dir

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


# run isabelle

PARENT=$(basename "$LOGIC")

[ -z "$BUILD" ] && cd "$NAME"

if [ "$DOCUMENT" != false -a -d document ]; then
  DOC="$DOCUMENT"
  [ -n "$DUMP" -a -d "$DUMP" ] && "$ISATOOL" latex -o sty "$DUMP/root.tex" >/dev/null
else
  DOC=""
fi


SECONDS=0

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

  OPT_C=""
  [ "$COMPRESS" = true ] && OPT_C="-c"

  "$ISABELLE" \
    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS;" \
    $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
  RC="$?"
else
  ITEM=$(basename "$LOGIC")-"$SESSION"
  echo "Running $ITEM ..."
  LOG="$LOGDIR/$ITEM"

  "$ISABELLE" \
    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS; 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 "Finished $ITEM ($ELAPSED elapsed time)"
  gzip --force "$LOG"
else
  echo "$ITEM FAILED"
  echo "(see also $LOG)"
  echo; tail "$LOG"; echo
fi

exit "$RC"