lib/Tools/build
author wenzelm
Fri Jul 27 23:14:55 2012 +0200 (2012-07-27)
changeset 48570 0c32d6267b93
parent 48546 f81cf2fcd3a0
child 48578 21361b6189a6
permissions -rwxr-xr-x
tuned message;
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@48474
    12
function show_settings()
wenzelm@48474
    13
{
wenzelm@48474
    14
  local PREFIX="$1"
wenzelm@48474
    15
  echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
wenzelm@48474
    16
  echo
wenzelm@48474
    17
  echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
wenzelm@48474
    18
  echo "${PREFIX}ML_HOME=\"$ML_HOME\""
wenzelm@48474
    19
  echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
wenzelm@48474
    20
  echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
wenzelm@48474
    21
}
wenzelm@48474
    22
wenzelm@48276
    23
function usage()
wenzelm@48276
    24
{
wenzelm@48276
    25
  echo
wenzelm@48276
    26
  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
wenzelm@48276
    27
  echo
wenzelm@48276
    28
  echo "  Options are:"
wenzelm@48570
    29
  echo "    -a           select all sessions"
wenzelm@48511
    30
  echo "    -b           build heap images"
wenzelm@48509
    31
  echo "    -d DIR       include session directory with ROOT file"
wenzelm@48570
    32
  echo "    -g NAME      select session group NAME"
wenzelm@48425
    33
  echo "    -j INT       maximum number of jobs (default 1)"
wenzelm@48469
    34
  echo "    -n           no build -- test dependencies only"
wenzelm@48276
    35
  echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
wenzelm@48447
    36
  echo "    -s           system build mode: produce output in ISABELLE_HOME"
wenzelm@48425
    37
  echo "    -v           verbose"
wenzelm@48276
    38
  echo
wenzelm@48276
    39
  echo "  Build and manage Isabelle sessions, depending on implicit"
wenzelm@48474
    40
  show_settings "  "
wenzelm@48276
    41
  echo
wenzelm@48276
    42
  exit 1
wenzelm@48276
    43
}
wenzelm@48276
    44
wenzelm@48276
    45
function fail()
wenzelm@48276
    46
{
wenzelm@48276
    47
  echo "$1" >&2
wenzelm@48276
    48
  exit 2
wenzelm@48276
    49
}
wenzelm@48276
    50
wenzelm@48425
    51
function check_number()
wenzelm@48425
    52
{
wenzelm@48425
    53
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
wenzelm@48425
    54
}
wenzelm@48425
    55
wenzelm@48276
    56
wenzelm@48276
    57
## process command line
wenzelm@48276
    58
wenzelm@48276
    59
ALL_SESSIONS=false
wenzelm@48511
    60
BUILD_HEAP=false
wenzelm@48509
    61
declare -a MORE_DIRS=()
wenzelm@48509
    62
declare -a SESSION_GROUPS=()
wenzelm@48425
    63
MAX_JOBS=1
wenzelm@48469
    64
NO_BUILD=false
wenzelm@48509
    65
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
wenzelm@48447
    66
SYSTEM_MODE=false
wenzelm@48425
    67
VERBOSE=false
wenzelm@48276
    68
wenzelm@48545
    69
while getopts "abd:g:j:no:sv" OPT
wenzelm@48276
    70
do
wenzelm@48276
    71
  case "$OPT" in
wenzelm@48276
    72
    a)
wenzelm@48276
    73
      ALL_SESSIONS="true"
wenzelm@48276
    74
      ;;
wenzelm@48276
    75
    b)
wenzelm@48511
    76
      BUILD_HEAP="true"
wenzelm@48276
    77
      ;;
wenzelm@48340
    78
    d)
wenzelm@48340
    79
      MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
wenzelm@48340
    80
      ;;
wenzelm@48509
    81
    g)
wenzelm@48509
    82
      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
wenzelm@48509
    83
      ;;
wenzelm@48425
    84
    j)
wenzelm@48425
    85
      check_number "$OPTARG"
wenzelm@48425
    86
      MAX_JOBS="$OPTARG"
wenzelm@48425
    87
      ;;
wenzelm@48469
    88
    n)
wenzelm@48469
    89
      NO_BUILD="true"
wenzelm@48276
    90
      ;;
wenzelm@48276
    91
    o)
wenzelm@48276
    92
      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
wenzelm@48276
    93
      ;;
wenzelm@48447
    94
    s)
wenzelm@48447
    95
      SYSTEM_MODE="true"
wenzelm@48447
    96
      ;;
wenzelm@48425
    97
    v)
wenzelm@48425
    98
      VERBOSE="true"
wenzelm@48425
    99
      ;;
wenzelm@48276
   100
    \?)
wenzelm@48276
   101
      usage
wenzelm@48276
   102
      ;;
wenzelm@48276
   103
  esac
wenzelm@48276
   104
done
wenzelm@48276
   105
wenzelm@48276
   106
shift $(($OPTIND - 1))
wenzelm@48276
   107
wenzelm@48276
   108
wenzelm@48276
   109
## main
wenzelm@48276
   110
wenzelm@48276
   111
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
wenzelm@48276
   112
wenzelm@48474
   113
if [ "$NO_BUILD" = false ]; then
wenzelm@48474
   114
  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
wenzelm@48474
   115
wenzelm@48474
   116
  if [ "$VERBOSE" = true ]; then
wenzelm@48474
   117
    show_settings ""
wenzelm@48474
   118
    echo
wenzelm@48474
   119
  fi
wenzelm@48474
   120
  . "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@48474
   121
fi
wenzelm@48474
   122
wenzelm@48474
   123
"$ISABELLE_TOOL" java isabelle.Build \
wenzelm@48545
   124
  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
wenzelm@48509
   125
  "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
wenzelm@48474
   126
RC="$?"
wenzelm@48474
   127
wenzelm@48474
   128
if [ "$NO_BUILD" = false ]; then
wenzelm@48474
   129
  echo -n "Finished at "; date
wenzelm@48474
   130
wenzelm@48474
   131
  . "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@48474
   132
  echo "$TIMES_REPORT"
wenzelm@48474
   133
fi
wenzelm@48474
   134
wenzelm@48474
   135
exit "$RC"