#!/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 "    -T LEVEL     multithreading: trace level (default 0)"

  echo "    -V VERSION   declare alternative document VERSION"

  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 "  HOL_USEDIR_OPTIONS=$HOL_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_VERSIONS=""

BUILD=""

DOCUMENT=false

ROOT_FILE="ROOT.ML"

DOCUMENT_GRAPH=false

INFO=false

MODES=""

RESET=false

SESSION=""

PROOFS="0"

PARALLEL_PROOFS="1"

TIMING=false

VERBOSE=false

function getoptions()

{

  OPTIND=1

  while getopts "C:D:M:P: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"

        ;;

      T)

        check_number "$OPTARG"

        TRACETHREADS="$OPTARG"

        ;;

      V)

        if [ -z "$DOCUMENT_VERSIONS" ]; then

          DOCUMENT_VERSIONS="\"$OPTARG\""

        else

          DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$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 \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS;" \

    -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 \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; 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 "$LOG"; echo; } >&2

fi

exit "$RC"