lib/Tools/build
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 50364 ce2796981c0c
child 51977 b55f90655328
permissions -rwxr-xr-x
tuned;
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
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    12
function show_settings()
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    13
{
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    14
  local PREFIX="$1"
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    15
  echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    16
  echo
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    17
  echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    18
  echo "${PREFIX}ML_HOME=\"$ML_HOME\""
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    19
  echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    20
  echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    21
}
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    22
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    23
function usage()
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    24
{
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    25
  echo
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    26
  echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
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 "  Options are:"
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    29
  echo "    -D DIR       include session directory and select its sessions"
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48903
diff changeset
    30
  echo "    -R           operate on requirements of selected sessions"
48570
0c32d6267b93 tuned message;
wenzelm
parents: 48546
diff changeset
    31
  echo "    -a           select all sessions"
48511
37999ee01156 remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents: 48509
diff changeset
    32
  echo "    -b           build heap images"
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
    33
  echo "    -c           clean build"
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    34
  echo "    -d DIR       include session directory"
48570
0c32d6267b93 tuned message;
wenzelm
parents: 48546
diff changeset
    35
  echo "    -g NAME      select session group NAME"
48578
21361b6189a6 some description of isabelle build;
wenzelm
parents: 48570
diff changeset
    36
  echo "    -j INT       maximum number of parallel jobs (default 1)"
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48780
diff changeset
    37
  echo "    -l           list session source files"
48469
826a771cff33 clarified build -n (no build);
wenzelm
parents: 48459
diff changeset
    38
  echo "    -n           no build -- test dependencies only"
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    39
  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
    40
  echo "    -s           system build mode: produce output in ISABELLE_HOME"
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    41
  echo "    -v           verbose"
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    42
  echo
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    43
  echo "  Build and manage Isabelle sessions, depending on implicit"
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
    44
  show_settings "  "
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    45
  echo
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    46
  exit 1
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    47
}
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    48
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    49
function fail()
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    50
{
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    51
  echo "$1" >&2
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    52
  exit 2
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    53
}
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    54
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    55
function check_number()
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    56
{
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    57
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    58
}
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    59
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    60
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    61
## process command line
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    62
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    63
declare -a SELECT_DIRS=()
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48903
diff changeset
    64
REQUIREMENTS=false
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    65
ALL_SESSIONS=false
48511
37999ee01156 remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents: 48509
diff changeset
    66
BUILD_HEAP=false
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
    67
CLEAN_BUILD=false
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    68
declare -a INCLUDE_DIRS=()
48509
4854ced3e9d7 support session groups;
wenzelm
parents: 48474
diff changeset
    69
declare -a SESSION_GROUPS=()
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    70
MAX_JOBS=1
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48780
diff changeset
    71
LIST_FILES=false
48469
826a771cff33 clarified build -n (no build);
wenzelm
parents: 48459
diff changeset
    72
NO_BUILD=false
48509
4854ced3e9d7 support session groups;
wenzelm
parents: 48474
diff changeset
    73
eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48425
diff changeset
    74
SYSTEM_MODE=false
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
    75
VERBOSE=false
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    76
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48903
diff changeset
    77
while getopts "D:Rabcd:g:j:lno:sv" OPT
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    78
do
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    79
  case "$OPT" in
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    80
    D)
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    81
      SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    82
      ;;
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48903
diff changeset
    83
    R)
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48903
diff changeset
    84
      REQUIREMENTS="true"
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48903
diff changeset
    85
      ;;
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    86
    a)
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    87
      ALL_SESSIONS="true"
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    88
      ;;
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    89
    b)
48511
37999ee01156 remove old output heaps, to ensure that result is valid wrt. check_stamps;
wenzelm
parents: 48509
diff changeset
    90
      BUILD_HEAP="true"
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
    91
      ;;
48595
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
    92
    c)
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
    93
      CLEAN_BUILD="true"
231e6fa96dbb added build option -c;
wenzelm
parents: 48594
diff changeset
    94
      ;;
48340
6f4fc030882a allow explicit specification of additional session directories;
wenzelm
parents: 48276
diff changeset
    95
    d)
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
    96
      INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
48340
6f4fc030882a allow explicit specification of additional session directories;
wenzelm
parents: 48276
diff changeset
    97
      ;;
48509
4854ced3e9d7 support session groups;
wenzelm
parents: 48474
diff changeset
    98
    g)
4854ced3e9d7 support session groups;
wenzelm
parents: 48474
diff changeset
    99
      SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
4854ced3e9d7 support session groups;
wenzelm
parents: 48474
diff changeset
   100
      ;;
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
   101
    j)
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
   102
      check_number "$OPTARG"
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
   103
      MAX_JOBS="$OPTARG"
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
   104
      ;;
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48780
diff changeset
   105
    l)
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48780
diff changeset
   106
      LIST_FILES="true"
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48780
diff changeset
   107
      ;;
48469
826a771cff33 clarified build -n (no build);
wenzelm
parents: 48459
diff changeset
   108
    n)
826a771cff33 clarified build -n (no build);
wenzelm
parents: 48459
diff changeset
   109
      NO_BUILD="true"
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   110
      ;;
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   111
    o)
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   112
      BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   113
      ;;
48447
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48425
diff changeset
   114
    s)
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48425
diff changeset
   115
      SYSTEM_MODE="true"
ef600ce4559c added system build mode: produce output in ISABELLE_HOME;
wenzelm
parents: 48425
diff changeset
   116
      ;;
48425
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
   117
    v)
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
   118
      VERBOSE="true"
0d95980e9aae parallel scheduling of jobs;
wenzelm
parents: 48340
diff changeset
   119
      ;;
48276
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   120
    \?)
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   121
      usage
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   122
      ;;
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   123
  esac
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   124
done
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   125
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   126
shift $(($OPTIND - 1))
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   127
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   128
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   129
## main
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   130
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   131
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
4bd480886813 basic setup for Isabelle build tool;
wenzelm
parents:
diff changeset
   132
48601
655b08c2cd89 less verbosity;
wenzelm
parents: 48595
diff changeset
   133
if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   134
  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   135
48601
655b08c2cd89 less verbosity;
wenzelm
parents: 48595
diff changeset
   136
  show_settings ""
655b08c2cd89 less verbosity;
wenzelm
parents: 48595
diff changeset
   137
  echo
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   138
fi
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   139
48780
49a965020394 always show some timing information, to reduce the need for explicit -v;
wenzelm
parents: 48737
diff changeset
   140
. "$ISABELLE_HOME/lib/scripts/timestart.bash"
49a965020394 always show some timing information, to reduce the need for explicit -v;
wenzelm
parents: 48737
diff changeset
   141
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   142
"$ISABELLE_TOOL" java isabelle.Build \
49131
aa1e2ba3c697 added build option -R;
wenzelm
parents: 48903
diff changeset
   143
  "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
48903
1621b3f26095 added build option -l (list files);
wenzelm
parents: 48780
diff changeset
   144
  "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
48737
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
   145
  "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
f3bbb9ca57d6 added build option -D: include session directory and select its sessions;
wenzelm
parents: 48601
diff changeset
   146
  "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   147
RC="$?"
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   148
48601
655b08c2cd89 less verbosity;
wenzelm
parents: 48595
diff changeset
   149
if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   150
  echo -n "Finished at "; date
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   151
fi
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   152
48780
49a965020394 always show some timing information, to reduce the need for explicit -v;
wenzelm
parents: 48737
diff changeset
   153
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
49a965020394 always show some timing information, to reduce the need for explicit -v;
wenzelm
parents: 48737
diff changeset
   154
echo "$TIMES_REPORT"
49a965020394 always show some timing information, to reduce the need for explicit -v;
wenzelm
parents: 48737
diff changeset
   155
48474
5b9d79c6323b tuned messages (cf. isabelle makeall);
wenzelm
parents: 48469
diff changeset
   156
exit "$RC"