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