lib/Tools/build
author wenzelm
Thu Jul 26 12:59:09 2012 +0200 (2012-07-26)
changeset 48511 37999ee01156
parent 48509 4854ced3e9d7
child 48545 c168bc64f2a8
permissions -rwxr-xr-x
remove old output heaps, to ensure that result is valid wrt. check_stamps;
tuned signature;
     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 "    -a           all sessions"
    30   echo "    -b           build heap images"
    31   echo "    -d DIR       include session directory with ROOT file"
    32   echo "    -g NAME      include session group NAME"
    33   echo "    -j INT       maximum number of jobs (default 1)"
    34   echo "    -n           no build -- test dependencies only"
    35   echo "    -o OPTION    override session configuration OPTION (via NAME=VAL or NAME)"
    36   echo "    -s           system build mode: produce output in ISABELLE_HOME"
    37   echo "    -t           inner session timing"
    38   echo "    -v           verbose"
    39   echo
    40   echo "  Build and manage Isabelle sessions, depending on implicit"
    41   show_settings "  "
    42   echo
    43   exit 1
    44 }
    45 
    46 function fail()
    47 {
    48   echo "$1" >&2
    49   exit 2
    50 }
    51 
    52 function check_number()
    53 {
    54   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    55 }
    56 
    57 
    58 ## process command line
    59 
    60 ALL_SESSIONS=false
    61 BUILD_HEAP=false
    62 declare -a MORE_DIRS=()
    63 declare -a SESSION_GROUPS=()
    64 MAX_JOBS=1
    65 NO_BUILD=false
    66 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    67 SYSTEM_MODE=false
    68 TIMING=false
    69 VERBOSE=false
    70 
    71 while getopts "abd:g:j:no:stv" OPT
    72 do
    73   case "$OPT" in
    74     a)
    75       ALL_SESSIONS="true"
    76       ;;
    77     b)
    78       BUILD_HEAP="true"
    79       ;;
    80     d)
    81       MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
    82       ;;
    83     g)
    84       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
    85       ;;
    86     j)
    87       check_number "$OPTARG"
    88       MAX_JOBS="$OPTARG"
    89       ;;
    90     n)
    91       NO_BUILD="true"
    92       ;;
    93     o)
    94       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
    95       ;;
    96     s)
    97       SYSTEM_MODE="true"
    98       ;;
    99     t)
   100       TIMING="true"
   101       ;;
   102     v)
   103       VERBOSE="true"
   104       ;;
   105     \?)
   106       usage
   107       ;;
   108   esac
   109 done
   110 
   111 shift $(($OPTIND - 1))
   112 
   113 
   114 ## main
   115 
   116 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
   117 
   118 if [ "$NO_BUILD" = false ]; then
   119   echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   120 
   121   if [ "$VERBOSE" = true ]; then
   122     show_settings ""
   123     echo
   124   fi
   125   . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   126 fi
   127 
   128 "$ISABELLE_TOOL" java isabelle.Build \
   129   "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \
   130   "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
   131 RC="$?"
   132 
   133 if [ "$NO_BUILD" = false ]; then
   134   echo -n "Finished at "; date
   135 
   136   . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   137   echo "$TIMES_REPORT"
   138 fi
   139 
   140 exit "$RC"