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