lib/Tools/build
author wenzelm
Mon Jul 30 11:03:44 2012 +0200 (2012-07-30)
changeset 48594 c24907e5081e
parent 48592 a125b8040ada
child 48595 231e6fa96dbb
permissions -rwxr-xr-x
removed build option -f (cf. a125b8040ada), due to slightly inconvenient behaviour on ancestors;
     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           select all sessions"
    30   echo "    -b           build heap images"
    31   echo "    -d DIR       include session directory with ROOT file"
    32   echo "    -g NAME      select session group NAME"
    33   echo "    -j INT       maximum number of parallel 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 "    -v           verbose"
    38   echo
    39   echo "  Build and manage Isabelle sessions, depending on implicit"
    40   show_settings "  "
    41   echo
    42   exit 1
    43 }
    44 
    45 function fail()
    46 {
    47   echo "$1" >&2
    48   exit 2
    49 }
    50 
    51 function check_number()
    52 {
    53   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    54 }
    55 
    56 
    57 ## process command line
    58 
    59 ALL_SESSIONS=false
    60 BUILD_HEAP=false
    61 declare -a MORE_DIRS=()
    62 declare -a SESSION_GROUPS=()
    63 MAX_JOBS=1
    64 NO_BUILD=false
    65 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    66 SYSTEM_MODE=false
    67 VERBOSE=false
    68 
    69 while getopts "abd:g:j:no:sv" OPT
    70 do
    71   case "$OPT" in
    72     a)
    73       ALL_SESSIONS="true"
    74       ;;
    75     b)
    76       BUILD_HEAP="true"
    77       ;;
    78     d)
    79       MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
    80       ;;
    81     g)
    82       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
    83       ;;
    84     j)
    85       check_number "$OPTARG"
    86       MAX_JOBS="$OPTARG"
    87       ;;
    88     n)
    89       NO_BUILD="true"
    90       ;;
    91     o)
    92       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
    93       ;;
    94     s)
    95       SYSTEM_MODE="true"
    96       ;;
    97     v)
    98       VERBOSE="true"
    99       ;;
   100     \?)
   101       usage
   102       ;;
   103   esac
   104 done
   105 
   106 shift $(($OPTIND - 1))
   107 
   108 
   109 ## main
   110 
   111 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
   112 
   113 if [ "$NO_BUILD" = false ]; then
   114   echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   115 
   116   if [ "$VERBOSE" = true ]; then
   117     show_settings ""
   118     echo
   119   fi
   120   . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   121 fi
   122 
   123 "$ISABELLE_TOOL" java isabelle.Build \
   124   "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   125   "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
   126 RC="$?"
   127 
   128 if [ "$NO_BUILD" = false ]; then
   129   echo -n "Finished at "; date
   130 
   131   . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   132   echo "$TIMES_REPORT"
   133 fi
   134 
   135 exit "$RC"