wneuper/isa: lib/Tools/build@37999ee01156

     1 #!/usr/bin/env bash

2 #

     3 # Author: Makarius

4 #

     5 # DESCRIPTION: build and manage Isabelle sessions

     8 ## diagnostics

    10 PRG="$(basename "$0")"

    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 }

    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 }

    46 function fail()

    47 {

    48   echo "$1" >&2

    49   exit 2

    50 }

    52 function check_number()

    53 {

    54   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""

    55 }

    58 ## process command line

    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

    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

   111 shift $(($OPTIND - 1))

   114 ## main

   116 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }

   118 if [ "$NO_BUILD" = false ]; then

   119   echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"

   121   if [ "$VERBOSE" = true ]; then

   122     show_settings ""

   123     echo

   124   fi

   125   . "$ISABELLE_HOME/lib/scripts/timestart.bash"

   126 fi

   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="$?"

   133 if [ "$NO_BUILD" = false ]; then

   134   echo -n "Finished at "; date

   136   . "$ISABELLE_HOME/lib/scripts/timestop.bash"

   137   echo "$TIMES_REPORT"

   138 fi

   140 exit "$RC"

author	wenzelm
	Thu, 26 Jul 2012 12:59:09 +0200
changeset 49526	37999ee01156
parent 49524	4854ced3e9d7
child 49560	c168bc64f2a8
permissions	-rwxr-xr-x