lib/Tools/build

documentation on last state of the art concerning interpretation

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: build and manage Isabelle sessions

## settings

case "$ISABELLE_JAVA_PLATFORM" in
  x86-*)
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
    ;;
  x86_64-*)
    ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
    ;;
esac


## diagnostics

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

function show_settings()
{
  local PREFIX="$1"
  echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
  echo
  echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_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 "    -D DIR       include session directory and select its sessions"
  echo "    -R           operate on requirements of selected sessions"
  echo "    -X NAME      exclude sessions from group NAME and all descendants"
  echo "    -a           select all sessions"
  echo "    -b           build heap images"
  echo "    -c           clean build"
  echo "    -d DIR       include session directory"
  echo "    -g NAME      select session group NAME"
  echo "    -j INT       maximum number of parallel jobs (default 1)"
  echo "    -k KEYWORD   check theory sources for conflicts with proposed keywords"
  echo "    -l           list session source files"
  echo "    -n           no build -- test dependencies only"
  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
  echo "    -s           system build mode: produce output in ISABELLE_HOME"
  echo "    -v           verbose"
  echo "    -x NAME      exclude session NAME and all descendants"
  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

declare -a SELECT_DIRS=()
REQUIREMENTS=false
declare -a EXCLUDE_SESSION_GROUPS=()
ALL_SESSIONS=false
BUILD_HEAP=false
CLEAN_BUILD=false
declare -a INCLUDE_DIRS=()
declare -a SESSION_GROUPS=()
MAX_JOBS=1
declare -a CHECK_KEYWORDS=()
LIST_FILES=false
NO_BUILD=false
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
SYSTEM_MODE=false
VERBOSE=false
declare -a EXCLUDE_SESSIONS=()

while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
do
  case "$OPT" in
    D)
      SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
      ;;
    R)
      REQUIREMENTS="true"
      ;;
    X)
      EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
      ;;
    a)
      ALL_SESSIONS="true"
      ;;
    b)
      BUILD_HEAP="true"
      ;;
    c)
      CLEAN_BUILD="true"
      ;;
    d)
      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
      ;;
    g)
      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
      ;;
    j)
      check_number "$OPTARG"
      MAX_JOBS="$OPTARG"
      ;;
    k)
      CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
      ;;
    l)
      LIST_FILES="true"
      ;;
    n)
      NO_BUILD="true"
      ;;
    o)
      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
      ;;
    s)
      SYSTEM_MODE="true"
      ;;
    v)
      VERBOSE="true"
      ;;
    x)
      EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


## main

isabelle_admin_build jars || exit $?

if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"

  show_settings ""
  echo
fi

declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"

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

"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
  "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
  "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
  "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
  "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
  "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
RC="$?"

if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
  echo -n "Finished at "; date
fi

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

exit "$RC"