#!/usr/bin/env bash

#

# Author: Makarius

#

# DESCRIPTION: build and manage Isabelle sessions

## diagnostics

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

function show_settings()

{

  local PREFIX="$1"

  echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""

  echo

  echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""

  echo "${PREFIX}ML_HOME=\"$ML_HOME\""

  echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""

  echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""

}

function usage()

{

  echo

  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"

  echo

  echo "  Options are:"

  echo "    -a           all sessions"

  echo "    -b           build heap images"

  echo "    -d DIR       include session directory with ROOT file"

  echo "    -g NAME      include session group NAME"

  echo "    -j INT       maximum number of jobs (default 1)"

  echo "    -n           no build -- test dependencies only"

  echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"

  echo "    -s           system build mode: produce output in ISABELLE_HOME"

  echo "    -t           inner session timing"

  echo "    -v           verbose"

  echo

  echo "  Build and manage Isabelle sessions, depending on implicit"

  show_settings "  "

  echo

  exit 1

}

function fail()

{

  echo "$1" >&2

  exit 2

}

function check_number()

{

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

}

## process command line

ALL_SESSIONS=false

BUILD_HEAP=false

declare -a MORE_DIRS=()

declare -a SESSION_GROUPS=()

MAX_JOBS=1

NO_BUILD=false

eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"

SYSTEM_MODE=false

TIMING=false

VERBOSE=false

while getopts "abd:g:j:no:stv" OPT

do

  case "$OPT" in

    a)

      ALL_SESSIONS="true"

      ;;

    b)

      BUILD_HEAP="true"

      ;;

    d)

      MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"

      ;;

    g)

      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"

      ;;

    j)

      check_number "$OPTARG"

      MAX_JOBS="$OPTARG"

      ;;

    n)

      NO_BUILD="true"

      ;;

    o)

      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"

      ;;

    s)

      SYSTEM_MODE="true"

      ;;

    t)

      TIMING="true"

      ;;

    v)

      VERBOSE="true"

      ;;

    \?)

      usage

      ;;

  esac

done

shift $(($OPTIND - 1))

## main

[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }

if [ "$NO_BUILD" = false ]; then

  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"

  if [ "$VERBOSE" = true ]; then

    show_settings ""

    echo

  fi

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

fi

"$ISABELLE_TOOL" java isabelle.Build \

  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \

  "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"

RC="$?"

if [ "$NO_BUILD" = false ]; then

  echo -n "Finished at "; date

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

  echo "$TIMES_REPORT"

fi

exit "$RC"