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

function getoptions()

{

  OPTIND=1

  while getopts "D:P:bc:d:i:m: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

        ;;

      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\";" \

    $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\"; 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"