lib/Tools/build
author wenzelm
Tue Jul 24 10:39:03 2012 +0200 (2012-07-24)
changeset 48459 375e45df6fdf
parent 48447 ef600ce4559c
child 48469 826a771cff33
permissions -rwxr-xr-x
timing is command line options, not system option;
wenzelm@48276
     1
#!/usr/bin/env bash
wenzelm@48276
     2
#
wenzelm@48276
     3
# Author: Makarius
wenzelm@48276
     4
#
wenzelm@48276
     5
# DESCRIPTION: build and manage Isabelle sessions
wenzelm@48276
     6
wenzelm@48276
     7
wenzelm@48276
     8
## diagnostics
wenzelm@48276
     9
wenzelm@48276
    10
PRG="$(basename "$0")"
wenzelm@48276
    11
wenzelm@48276
    12
function usage()
wenzelm@48276
    13
{
wenzelm@48276
    14
  echo
wenzelm@48276
    15
  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
wenzelm@48276
    16
  echo
wenzelm@48276
    17
  echo "  Options are:"
wenzelm@48276
    18
  echo "    -a           all sessions"
wenzelm@48276
    19
  echo "    -b           build target images"
wenzelm@48340
    20
  echo "    -d DIR       additional session directory with ROOT file"
wenzelm@48425
    21
  echo "    -j INT       maximum number of jobs (default 1)"
wenzelm@48276
    22
  echo "    -l           list sessions only"
wenzelm@48276
    23
  echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
wenzelm@48447
    24
  echo "    -s           system build mode: produce output in ISABELLE_HOME"
wenzelm@48459
    25
  echo "    -t           inner session timing"
wenzelm@48425
    26
  echo "    -v           verbose"
wenzelm@48276
    27
  echo
wenzelm@48276
    28
  echo "  Build and manage Isabelle sessions, depending on implicit"
wenzelm@48276
    29
  echo "  ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
wenzelm@48276
    30
  echo
wenzelm@48276
    31
  echo "  ML_PLATFORM=\"$ML_PLATFORM\""
wenzelm@48276
    32
  echo "  ML_HOME=\"$ML_HOME\""
wenzelm@48276
    33
  echo "  ML_SYSTEM=\"$ML_SYSTEM\""
wenzelm@48276
    34
  echo "  ML_OPTIONS=\"$ML_OPTIONS\""
wenzelm@48276
    35
  echo
wenzelm@48276
    36
  exit 1
wenzelm@48276
    37
}
wenzelm@48276
    38
wenzelm@48276
    39
function fail()
wenzelm@48276
    40
{
wenzelm@48276
    41
  echo "$1" >&2
wenzelm@48276
    42
  exit 2
wenzelm@48276
    43
}
wenzelm@48276
    44
wenzelm@48425
    45
function check_number()
wenzelm@48425
    46
{
wenzelm@48425
    47
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
wenzelm@48425
    48
}
wenzelm@48425
    49
wenzelm@48276
    50
wenzelm@48276
    51
## process command line
wenzelm@48276
    52
wenzelm@48276
    53
ALL_SESSIONS=false
wenzelm@48276
    54
BUILD_IMAGES=false
wenzelm@48425
    55
MAX_JOBS=1
wenzelm@48276
    56
LIST_ONLY=false
wenzelm@48447
    57
SYSTEM_MODE=false
wenzelm@48459
    58
TIMING=false
wenzelm@48425
    59
VERBOSE=false
wenzelm@48276
    60
wenzelm@48340
    61
declare -a MORE_DIRS=()
wenzelm@48276
    62
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
wenzelm@48276
    63
wenzelm@48459
    64
while getopts "abd:j:lo:stv" OPT
wenzelm@48276
    65
do
wenzelm@48276
    66
  case "$OPT" in
wenzelm@48276
    67
    a)
wenzelm@48276
    68
      ALL_SESSIONS="true"
wenzelm@48276
    69
      ;;
wenzelm@48276
    70
    b)
wenzelm@48276
    71
      BUILD_IMAGES="true"
wenzelm@48276
    72
      ;;
wenzelm@48340
    73
    d)
wenzelm@48340
    74
      MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
wenzelm@48340
    75
      ;;
wenzelm@48425
    76
    j)
wenzelm@48425
    77
      check_number "$OPTARG"
wenzelm@48425
    78
      MAX_JOBS="$OPTARG"
wenzelm@48425
    79
      ;;
wenzelm@48276
    80
    l)
wenzelm@48276
    81
      LIST_ONLY="true"
wenzelm@48276
    82
      ;;
wenzelm@48276
    83
    o)
wenzelm@48276
    84
      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
wenzelm@48276
    85
      ;;
wenzelm@48447
    86
    s)
wenzelm@48447
    87
      SYSTEM_MODE="true"
wenzelm@48447
    88
      ;;
wenzelm@48459
    89
    t)
wenzelm@48459
    90
      TIMING="true"
wenzelm@48459
    91
      ;;
wenzelm@48425
    92
    v)
wenzelm@48425
    93
      VERBOSE="true"
wenzelm@48425
    94
      ;;
wenzelm@48276
    95
    \?)
wenzelm@48276
    96
      usage
wenzelm@48276
    97
      ;;
wenzelm@48276
    98
  esac
wenzelm@48276
    99
done
wenzelm@48276
   100
wenzelm@48276
   101
shift $(($OPTIND - 1))
wenzelm@48276
   102
wenzelm@48276
   103
wenzelm@48276
   104
## main
wenzelm@48276
   105
wenzelm@48276
   106
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
wenzelm@48276
   107
wenzelm@48276
   108
exec "$ISABELLE_TOOL" java isabelle.Build \
wenzelm@48459
   109
  "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$TIMING" \
wenzelm@48459
   110
  "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"