lib/Tools/build
author wenzelm
Fri May 17 19:04:52 2013 +0200 (2013-05-17)
changeset 52056 fc458f304f93
parent 51977 b55f90655328
child 52443 725916b7dee5
permissions -rwxr-xr-x
added isabelle-process option -o;
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@48737
    29
  echo "    -D DIR       include session directory and select its sessions"
wenzelm@49131
    30
  echo "    -R           operate on requirements of selected sessions"
wenzelm@48570
    31
  echo "    -a           select all sessions"
wenzelm@48511
    32
  echo "    -b           build heap images"
wenzelm@48595
    33
  echo "    -c           clean build"
wenzelm@48737
    34
  echo "    -d DIR       include session directory"
wenzelm@48570
    35
  echo "    -g NAME      select session group NAME"
wenzelm@48578
    36
  echo "    -j INT       maximum number of parallel jobs (default 1)"
wenzelm@48903
    37
  echo "    -l           list session source files"
wenzelm@48469
    38
  echo "    -n           no build -- test dependencies only"
wenzelm@52056
    39
  echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
wenzelm@48447
    40
  echo "    -s           system build mode: produce output in ISABELLE_HOME"
wenzelm@48425
    41
  echo "    -v           verbose"
wenzelm@48276
    42
  echo
wenzelm@48276
    43
  echo "  Build and manage Isabelle sessions, depending on implicit"
wenzelm@48474
    44
  show_settings "  "
wenzelm@48276
    45
  echo
wenzelm@48276
    46
  exit 1
wenzelm@48276
    47
}
wenzelm@48276
    48
wenzelm@48276
    49
function fail()
wenzelm@48276
    50
{
wenzelm@48276
    51
  echo "$1" >&2
wenzelm@48276
    52
  exit 2
wenzelm@48276
    53
}
wenzelm@48276
    54
wenzelm@48425
    55
function check_number()
wenzelm@48425
    56
{
wenzelm@48425
    57
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
wenzelm@48425
    58
}
wenzelm@48425
    59
wenzelm@48276
    60
wenzelm@48276
    61
## process command line
wenzelm@48276
    62
wenzelm@48737
    63
declare -a SELECT_DIRS=()
wenzelm@49131
    64
REQUIREMENTS=false
wenzelm@48276
    65
ALL_SESSIONS=false
wenzelm@48511
    66
BUILD_HEAP=false
wenzelm@48595
    67
CLEAN_BUILD=false
wenzelm@48737
    68
declare -a INCLUDE_DIRS=()
wenzelm@48509
    69
declare -a SESSION_GROUPS=()
wenzelm@48425
    70
MAX_JOBS=1
wenzelm@48903
    71
LIST_FILES=false
wenzelm@48469
    72
NO_BUILD=false
wenzelm@48509
    73
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
wenzelm@48447
    74
SYSTEM_MODE=false
wenzelm@48425
    75
VERBOSE=false
wenzelm@48276
    76
wenzelm@49131
    77
while getopts "D:Rabcd:g:j:lno:sv" OPT
wenzelm@48276
    78
do
wenzelm@48276
    79
  case "$OPT" in
wenzelm@48737
    80
    D)
wenzelm@48737
    81
      SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
wenzelm@48737
    82
      ;;
wenzelm@49131
    83
    R)
wenzelm@49131
    84
      REQUIREMENTS="true"
wenzelm@49131
    85
      ;;
wenzelm@48276
    86
    a)
wenzelm@48276
    87
      ALL_SESSIONS="true"
wenzelm@48276
    88
      ;;
wenzelm@48276
    89
    b)
wenzelm@48511
    90
      BUILD_HEAP="true"
wenzelm@48276
    91
      ;;
wenzelm@48595
    92
    c)
wenzelm@48595
    93
      CLEAN_BUILD="true"
wenzelm@48595
    94
      ;;
wenzelm@48340
    95
    d)
wenzelm@48737
    96
      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
wenzelm@48340
    97
      ;;
wenzelm@48509
    98
    g)
wenzelm@48509
    99
      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
wenzelm@48509
   100
      ;;
wenzelm@48425
   101
    j)
wenzelm@48425
   102
      check_number "$OPTARG"
wenzelm@48425
   103
      MAX_JOBS="$OPTARG"
wenzelm@48425
   104
      ;;
wenzelm@48903
   105
    l)
wenzelm@48903
   106
      LIST_FILES="true"
wenzelm@48903
   107
      ;;
wenzelm@48469
   108
    n)
wenzelm@48469
   109
      NO_BUILD="true"
wenzelm@48276
   110
      ;;
wenzelm@48276
   111
    o)
wenzelm@48276
   112
      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
wenzelm@48276
   113
      ;;
wenzelm@48447
   114
    s)
wenzelm@48447
   115
      SYSTEM_MODE="true"
wenzelm@48447
   116
      ;;
wenzelm@48425
   117
    v)
wenzelm@48425
   118
      VERBOSE="true"
wenzelm@48425
   119
      ;;
wenzelm@48276
   120
    \?)
wenzelm@48276
   121
      usage
wenzelm@48276
   122
      ;;
wenzelm@48276
   123
  esac
wenzelm@48276
   124
done
wenzelm@48276
   125
wenzelm@48276
   126
shift $(($OPTIND - 1))
wenzelm@48276
   127
wenzelm@48276
   128
wenzelm@48276
   129
## main
wenzelm@48276
   130
wenzelm@48276
   131
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
wenzelm@48276
   132
wenzelm@48601
   133
if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
wenzelm@48474
   134
  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
wenzelm@48474
   135
wenzelm@48601
   136
  show_settings ""
wenzelm@48601
   137
  echo
wenzelm@48474
   138
fi
wenzelm@48474
   139
wenzelm@51977
   140
declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
wenzelm@51977
   141
wenzelm@48780
   142
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@48780
   143
wenzelm@51977
   144
"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
wenzelm@49131
   145
  "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
wenzelm@48903
   146
  "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
wenzelm@48737
   147
  "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
wenzelm@48737
   148
  "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
wenzelm@48474
   149
RC="$?"
wenzelm@48474
   150
wenzelm@48601
   151
if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
wenzelm@48474
   152
  echo -n "Finished at "; date
wenzelm@48474
   153
fi
wenzelm@48474
   154
wenzelm@48780
   155
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@48780
   156
echo "$TIMES_REPORT"
wenzelm@48780
   157
wenzelm@48474
   158
exit "$RC"