lib/Tools/build
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 61135 8f7d802b7a71
child 62589 b5783412bfed
permissions -rwxr-xr-x
updated for release;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # DESCRIPTION: build and manage Isabelle sessions
     6 
     7 ## settings
     8 
     9 case "$ISABELLE_JAVA_PLATFORM" in
    10   x86-*)
    11     ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
    12     ;;
    13   x86_64-*)
    14     ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
    15     ;;
    16 esac
    17 
    18 
    19 ## diagnostics
    20 
    21 PRG="$(basename "$0")"
    22 
    23 function show_settings()
    24 {
    25   local PREFIX="$1"
    26   echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
    27   echo
    28   echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_OPTIONS\""
    29   echo
    30   echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
    31   echo "${PREFIX}ML_HOME=\"$ML_HOME\""
    32   echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
    33   echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
    34 }
    35 
    36 function usage()
    37 {
    38   echo
    39   echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
    40   echo
    41   echo "  Options are:"
    42   echo "    -D DIR       include session directory and select its sessions"
    43   echo "    -R           operate on requirements of selected sessions"
    44   echo "    -X NAME      exclude sessions from group NAME and all descendants"
    45   echo "    -a           select all sessions"
    46   echo "    -b           build heap images"
    47   echo "    -c           clean build"
    48   echo "    -d DIR       include session directory"
    49   echo "    -g NAME      select session group NAME"
    50   echo "    -j INT       maximum number of parallel jobs (default 1)"
    51   echo "    -k KEYWORD   check theory sources for conflicts with proposed keywords"
    52   echo "    -l           list session source files"
    53   echo "    -n           no build -- test dependencies only"
    54   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    55   echo "    -s           system build mode: produce output in ISABELLE_HOME"
    56   echo "    -v           verbose"
    57   echo "    -x NAME      exclude session NAME and all descendants"
    58   echo
    59   echo "  Build and manage Isabelle sessions, depending on implicit"
    60   show_settings "  "
    61   echo
    62   exit 1
    63 }
    64 
    65 function fail()
    66 {
    67   echo "$1" >&2
    68   exit 2
    69 }
    70 
    71 function check_number()
    72 {
    73   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    74 }
    75 
    76 
    77 ## process command line
    78 
    79 declare -a SELECT_DIRS=()
    80 REQUIREMENTS=false
    81 declare -a EXCLUDE_SESSION_GROUPS=()
    82 ALL_SESSIONS=false
    83 BUILD_HEAP=false
    84 CLEAN_BUILD=false
    85 declare -a INCLUDE_DIRS=()
    86 declare -a SESSION_GROUPS=()
    87 MAX_JOBS=1
    88 declare -a CHECK_KEYWORDS=()
    89 LIST_FILES=false
    90 NO_BUILD=false
    91 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    92 SYSTEM_MODE=false
    93 VERBOSE=false
    94 declare -a EXCLUDE_SESSIONS=()
    95 
    96 while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT
    97 do
    98   case "$OPT" in
    99     D)
   100       SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
   101       ;;
   102     R)
   103       REQUIREMENTS="true"
   104       ;;
   105     X)
   106       EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG"
   107       ;;
   108     a)
   109       ALL_SESSIONS="true"
   110       ;;
   111     b)
   112       BUILD_HEAP="true"
   113       ;;
   114     c)
   115       CLEAN_BUILD="true"
   116       ;;
   117     d)
   118       INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
   119       ;;
   120     g)
   121       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
   122       ;;
   123     j)
   124       check_number "$OPTARG"
   125       MAX_JOBS="$OPTARG"
   126       ;;
   127     k)
   128       CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
   129       ;;
   130     l)
   131       LIST_FILES="true"
   132       ;;
   133     n)
   134       NO_BUILD="true"
   135       ;;
   136     o)
   137       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
   138       ;;
   139     s)
   140       SYSTEM_MODE="true"
   141       ;;
   142     v)
   143       VERBOSE="true"
   144       ;;
   145     x)
   146       EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
   147       ;;
   148     \?)
   149       usage
   150       ;;
   151   esac
   152 done
   153 
   154 shift $(($OPTIND - 1))
   155 
   156 
   157 ## main
   158 
   159 isabelle_admin_build jars || exit $?
   160 
   161 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   162   echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   163 
   164   show_settings ""
   165   echo
   166 fi
   167 
   168 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
   169 
   170 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   171 
   172 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
   173   "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   174   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   175   "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
   176   "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
   177   "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \
   178   "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
   179 RC="$?"
   180 
   181 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   182   echo -n "Finished at "; date
   183 fi
   184 
   185 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   186 echo "$TIMES_REPORT"
   187 
   188 exit "$RC"