lib/Tools/build
author wenzelm
Wed Dec 05 14:13:47 2012 +0100 (2012-12-05)
changeset 50364 ce2796981c0c
parent 49131 aa1e2ba3c697
child 51977 b55f90655328
permissions -rwxr-xr-x
tuned;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # DESCRIPTION: build and manage Isabelle sessions
     6 
     7 
     8 ## diagnostics
     9 
    10 PRG="$(basename "$0")"
    11 
    12 function show_settings()
    13 {
    14   local PREFIX="$1"
    15   echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\""
    16   echo
    17   echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\""
    18   echo "${PREFIX}ML_HOME=\"$ML_HOME\""
    19   echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\""
    20   echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\""
    21 }
    22 
    23 function usage()
    24 {
    25   echo
    26   echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]"
    27   echo
    28   echo "  Options are:"
    29   echo "    -D DIR       include session directory and select its sessions"
    30   echo "    -R           operate on requirements of selected sessions"
    31   echo "    -a           select all sessions"
    32   echo "    -b           build heap images"
    33   echo "    -c           clean build"
    34   echo "    -d DIR       include session directory"
    35   echo "    -g NAME      select session group NAME"
    36   echo "    -j INT       maximum number of parallel jobs (default 1)"
    37   echo "    -l           list session source files"
    38   echo "    -n           no build -- test dependencies only"
    39   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
    40   echo "    -s           system build mode: produce output in ISABELLE_HOME"
    41   echo "    -v           verbose"
    42   echo
    43   echo "  Build and manage Isabelle sessions, depending on implicit"
    44   show_settings "  "
    45   echo
    46   exit 1
    47 }
    48 
    49 function fail()
    50 {
    51   echo "$1" >&2
    52   exit 2
    53 }
    54 
    55 function check_number()
    56 {
    57   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    58 }
    59 
    60 
    61 ## process command line
    62 
    63 declare -a SELECT_DIRS=()
    64 REQUIREMENTS=false
    65 ALL_SESSIONS=false
    66 BUILD_HEAP=false
    67 CLEAN_BUILD=false
    68 declare -a INCLUDE_DIRS=()
    69 declare -a SESSION_GROUPS=()
    70 MAX_JOBS=1
    71 LIST_FILES=false
    72 NO_BUILD=false
    73 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    74 SYSTEM_MODE=false
    75 VERBOSE=false
    76 
    77 while getopts "D:Rabcd:g:j:lno:sv" OPT
    78 do
    79   case "$OPT" in
    80     D)
    81       SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
    82       ;;
    83     R)
    84       REQUIREMENTS="true"
    85       ;;
    86     a)
    87       ALL_SESSIONS="true"
    88       ;;
    89     b)
    90       BUILD_HEAP="true"
    91       ;;
    92     c)
    93       CLEAN_BUILD="true"
    94       ;;
    95     d)
    96       INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
    97       ;;
    98     g)
    99       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
   100       ;;
   101     j)
   102       check_number "$OPTARG"
   103       MAX_JOBS="$OPTARG"
   104       ;;
   105     l)
   106       LIST_FILES="true"
   107       ;;
   108     n)
   109       NO_BUILD="true"
   110       ;;
   111     o)
   112       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
   113       ;;
   114     s)
   115       SYSTEM_MODE="true"
   116       ;;
   117     v)
   118       VERBOSE="true"
   119       ;;
   120     \?)
   121       usage
   122       ;;
   123   esac
   124 done
   125 
   126 shift $(($OPTIND - 1))
   127 
   128 
   129 ## main
   130 
   131 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
   132 
   133 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   134   echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   135 
   136   show_settings ""
   137   echo
   138 fi
   139 
   140 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   141 
   142 "$ISABELLE_TOOL" java isabelle.Build \
   143   "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   144   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   145   "${SELECT_DIRS[@]}" $'\n' "${INCLUDE_DIRS[@]}" $'\n' \
   146   "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
   147 RC="$?"
   148 
   149 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   150   echo -n "Finished at "; date
   151 fi
   152 
   153 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   154 echo "$TIMES_REPORT"
   155 
   156 exit "$RC"