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