#!/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

   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 -40 "$LOG"; echo; } >&2

 fi

 exit "$RC"