lib/Tools/usedir

more informative errors for 'proof' and 'apply' steps;
more Seq.result operations;

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: build object-logic or run examples


## diagnostics

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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME"
  echo
  echo "  Options are:"
  echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
  echo "    -D PATH      dump generated document sources into PATH"
  echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
  echo "    -P PATH      set path for remote theory browsing information"
  echo "    -Q INT       set threshold for sub-proof parallelization (default 100)"
  echo "    -T LEVEL     multithreading: trace level (default 0)"
  echo "    -V VARIANT   declare alternative document VARIANT"
  echo "    -b           build mode (output heap image, using current dir)"
  echo "    -d FORMAT    build document as FORMAT (default false)"
  echo "    -f NAME      use ML file NAME (default ROOT.ML)"
  echo "    -g BOOL      generate session graph image for document (default false)"
  echo "    -i BOOL      generate HTML and graph browser information (default false)"
  echo "    -m MODE      add print mode for output"
  echo "    -p LEVEL     set level of detail for proof objects (default 0)"
  echo "    -q LEVEL     set level of parallel proof checking (default 1)"
  echo "    -r           reset session path"
  echo "    -s NAME      override session NAME"
  echo "    -t BOOL      internal session timing (default false)"
  echo "    -v BOOL      be verbose (default false)"
  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
  echo "  ML_PLATFORM=$ML_PLATFORM"
  echo "  ML_HOME=$ML_HOME"
  echo "  ML_SYSTEM=$ML_SYSTEM"
  echo "  ML_OPTIONS=$ML_OPTIONS"
  echo
  exit 1
}

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

function check_bool()
{
  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
}

function check_number()
{
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
}


## process command line

# options

COPY_DUMP=true
DUMP=""
MAXTHREADS="1"
RPATH=""
TRACETHREADS="0"
DOCUMENT_VARIANTS=""
BUILD=""
DOCUMENT=false
ROOT_FILE="ROOT.ML"
DOCUMENT_GRAPH=false
INFO=false
MODES=""
RESET=false
SESSION=""
PROOFS="0"
PARALLEL_PROOFS="1"
PARALLEL_PROOFS_THRESHOLD="100"
TIMING=false
VERBOSE=false

function getoptions()
{
  OPTIND=1
  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
  do
    case "$OPT" in
      C)
        check_bool "$OPTARG"
        COPY_DUMP="$OPTARG"
        ;;
      D)
        DUMP="$OPTARG"
        ;;
      M)
        if [ "$OPTARG" = max ]; then
          MAXTHREADS=0
        else
          check_number "$OPTARG"
          MAXTHREADS="$OPTARG"
        fi
        ;;
      P)
        RPATH="$OPTARG"
        ;;
      Q)
        check_number "$OPTARG"
        PARALLEL_PROOFS_THRESHOLD="$OPTARG"
        ;;
      T)
        check_number "$OPTARG"
        TRACETHREADS="$OPTARG"
        ;;
      V)
        if [ -z "$DOCUMENT_VARIANTS" ]; then
          DOCUMENT_VARIANTS="\"$OPTARG\""
        else
          DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
        fi
        ;;
      b)
        BUILD=true
        ;;
      d)
        DOCUMENT="$OPTARG"
        ;;
      f)
        ROOT_FILE="$OPTARG"
        ;;
      g)
        check_bool "$OPTARG"
        DOCUMENT_GRAPH="$OPTARG"
        ;;
      i)
        check_bool "$OPTARG"
        INFO="$OPTARG"
        ;;
      m)
        if [ -z "$MODES" ]; then
          MODES="\"$OPTARG\""
        else
          MODES="\"$OPTARG\", $MODES"
        fi
        ;;
      p)
        check_number "$OPTARG"
        PROOFS="$OPTARG"
        ;;
      q)
        check_number "$OPTARG"
        PARALLEL_PROOFS="$OPTARG"
        ;;
      r)
        RESET=true
        ;;
      s)
        SESSION="$OPTARG"
        ;;
      t)
        check_bool "$OPTARG"
        TIMING="$OPTARG"
        ;;
      v)
        check_bool "$OPTARG"
        VERBOSE="$OPTARG"
        ;;
      \?)
        usage
        ;;
    esac
  done
}

eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
getoptions "${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"
  cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
    "$ISABELLE_HOME/lib/html/library_index_content.template" \
    "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
fi


# prepare log dir

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


# run isabelle

PARENT=$(basename "$LOGIC")

if [ -z "$BUILD" ]; then
  cd "$NAME" || fail "Bad session directory '$NAME'"
fi

if [ "$DOCUMENT" != false ]; then
  DOC="$DOCUMENT"
else
  DOC=""
fi


. "$ISABELLE_HOME/lib/scripts/timestart.bash"

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

  "$ISABELLE_PROCESS" \
    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
    -q -w $LOGIC $NAME > "$LOG"
  RC="$?"
else
  ITEM=$(basename "$LOGIC")-"$SESSION"
  echo "Running $ITEM ..." >&2
  LOG="$LOGDIR/$ITEM"

  "$ISABELLE_PROCESS" \
    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
    -r -q "$LOGIC" > "$LOG"
  RC="$?"
  cd ..
fi

. "$ISABELLE_HOME/lib/scripts/timestop.bash"


# exit status

if [ "$RC" -eq 0 ]; then
  echo "Finished $ITEM ($TIMES_REPORT)" >&2
  gzip --force "$LOG"
else
  { echo "$ITEM FAILED";
    echo "(see also $LOG)";
    echo; tail -20 "$LOG"; echo; } >&2
fi

exit "$RC"