lib/Tools/build
author wenzelm
Wed Apr 01 15:41:08 2015 +0200 (2015-04-01)
changeset 59891 9ce697050455
parent 59565 96e860a17b9a
child 59892 2a616319c171
permissions -rwxr-xr-x
added isabelle build option -k, for fast off-line checking of theory sources;
     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 "    -k KEYWORD   check theory sources for conflicts with proposed keywords"
    38   echo "    -l           list session source files"
    39   echo "    -n           no build -- test dependencies only"
    40   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
    41   echo "    -s           system build mode: produce output in ISABELLE_HOME"
    42   echo "    -v           verbose"
    43   echo
    44   echo "  Build and manage Isabelle sessions, depending on implicit"
    45   show_settings "  "
    46   echo
    47   exit 1
    48 }
    49 
    50 function fail()
    51 {
    52   echo "$1" >&2
    53   exit 2
    54 }
    55 
    56 function check_number()
    57 {
    58   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    59 }
    60 
    61 
    62 ## process command line
    63 
    64 declare -a SELECT_DIRS=()
    65 REQUIREMENTS=false
    66 ALL_SESSIONS=false
    67 BUILD_HEAP=false
    68 CLEAN_BUILD=false
    69 declare -a INCLUDE_DIRS=()
    70 declare -a SESSION_GROUPS=()
    71 MAX_JOBS=1
    72 declare -a CHECK_KEYWORDS=()
    73 LIST_FILES=false
    74 NO_BUILD=false
    75 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    76 SYSTEM_MODE=false
    77 VERBOSE=false
    78 
    79 while getopts "D:Rabcd:g:j:k:lno:sv" OPT
    80 do
    81   case "$OPT" in
    82     D)
    83       SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG"
    84       ;;
    85     R)
    86       REQUIREMENTS="true"
    87       ;;
    88     a)
    89       ALL_SESSIONS="true"
    90       ;;
    91     b)
    92       BUILD_HEAP="true"
    93       ;;
    94     c)
    95       CLEAN_BUILD="true"
    96       ;;
    97     d)
    98       INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
    99       ;;
   100     g)
   101       SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG"
   102       ;;
   103     j)
   104       check_number "$OPTARG"
   105       MAX_JOBS="$OPTARG"
   106       ;;
   107     k)
   108       CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
   109       ;;
   110     l)
   111       LIST_FILES="true"
   112       ;;
   113     n)
   114       NO_BUILD="true"
   115       ;;
   116     o)
   117       BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG"
   118       ;;
   119     s)
   120       SYSTEM_MODE="true"
   121       ;;
   122     v)
   123       VERBOSE="true"
   124       ;;
   125     \?)
   126       usage
   127       ;;
   128   esac
   129 done
   130 
   131 shift $(($OPTIND - 1))
   132 
   133 
   134 ## main
   135 
   136 isabelle_admin_build jars || exit $?
   137 
   138 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   139   echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
   140 
   141   show_settings ""
   142   echo
   143 fi
   144 
   145 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
   146 
   147 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   148 
   149 "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
   150   "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   151   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   152   "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
   153   "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
   154   "${BUILD_OPTIONS[@]}" $'\n' "$@"
   155 RC="$?"
   156 
   157 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
   158   echo -n "Finished at "; date
   159 fi
   160 
   161 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   162 echo "$TIMES_REPORT"
   163 
   164 exit "$RC"