# HG changeset patch # User wenzelm # Date 1457644184 -3600 # Node ID 0c837beeb5e778aecdc586c2e2e06624050203a5 # Parent b5783412bfed093ebea036da272c7c9370f325fb upgrade "isabelle build" to Isabelle/Scala; diff -r b5783412bfed -r 0c837beeb5e7 lib/Tools/build --- a/lib/Tools/build Thu Mar 10 17:30:04 2016 +0100 +++ b/lib/Tools/build Thu Mar 10 22:09:44 2016 +0100 @@ -4,7 +4,7 @@ # # DESCRIPTION: build and manage Isabelle sessions -## settings +isabelle_admin_build jars || exit $? case "$ISABELLE_JAVA_PLATFORM" in x86-*) @@ -15,174 +15,6 @@ ;; esac - -## diagnostics - -PRG="$(basename "$0")" - -function show_settings() -{ - local PREFIX="$1" - echo "${PREFIX}ISABELLE_BUILD_OPTIONS=\"$ISABELLE_BUILD_OPTIONS\"" - echo - echo "${PREFIX}ISABELLE_BUILD_JAVA_OPTIONS=\"$ISABELLE_BUILD_JAVA_OPTIONS\"" - echo - echo "${PREFIX}ML_PLATFORM=\"$ML_PLATFORM\"" - echo "${PREFIX}ML_HOME=\"$ML_HOME\"" - echo "${PREFIX}ML_SYSTEM=\"$ML_SYSTEM\"" - echo "${PREFIX}ML_OPTIONS=\"$ML_OPTIONS\"" -} - -function usage() -{ - echo - echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]" - echo - echo " Options are:" - echo " -D DIR include session directory and select its sessions" - echo " -R operate on requirements of selected sessions" - echo " -X NAME exclude sessions from group NAME and all descendants" - echo " -a select all sessions" - echo " -b build heap images" - echo " -c clean build" - echo " -d DIR include session directory" - echo " -g NAME select session group NAME" - echo " -j INT maximum number of parallel jobs (default 1)" - echo " -k KEYWORD check theory sources for conflicts with proposed keywords" - echo " -l list session source files" - echo " -n no build -- test dependencies only" - echo " -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)" - echo " -s system build mode: produce output in ISABELLE_HOME" - echo " -v verbose" - echo " -x NAME exclude session NAME and all descendants" - echo - echo " Build and manage Isabelle sessions, depending on implicit" - show_settings " " - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - -function check_number() -{ - [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" -} - - -## process command line - -declare -a SELECT_DIRS=() -REQUIREMENTS=false -declare -a EXCLUDE_SESSION_GROUPS=() -ALL_SESSIONS=false -BUILD_HEAP=false -CLEAN_BUILD=false -declare -a INCLUDE_DIRS=() -declare -a SESSION_GROUPS=() -MAX_JOBS=1 -declare -a CHECK_KEYWORDS=() -LIST_FILES=false -NO_BUILD=false -eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" -SYSTEM_MODE=false -VERBOSE=false -declare -a EXCLUDE_SESSIONS=() +eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" -while getopts "D:RX:abcd:g:j:k:lno:svx:" OPT -do - case "$OPT" in - D) - SELECT_DIRS["${#SELECT_DIRS[@]}"]="$OPTARG" - ;; - R) - REQUIREMENTS="true" - ;; - X) - EXCLUDE_SESSION_GROUPS["${#EXCLUDE_SESSION_GROUPS[@]}"]="$OPTARG" - ;; - a) - ALL_SESSIONS="true" - ;; - b) - BUILD_HEAP="true" - ;; - c) - CLEAN_BUILD="true" - ;; - d) - INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG" - ;; - g) - SESSION_GROUPS["${#SESSION_GROUPS[@]}"]="$OPTARG" - ;; - j) - check_number "$OPTARG" - MAX_JOBS="$OPTARG" - ;; - k) - CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG" - ;; - l) - LIST_FILES="true" - ;; - n) - NO_BUILD="true" - ;; - o) - BUILD_OPTIONS["${#BUILD_OPTIONS[@]}"]="$OPTARG" - ;; - s) - SYSTEM_MODE="true" - ;; - v) - VERBOSE="true" - ;; - x) - EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG" - ;; - \?) - usage - ;; - esac -done - -shift $(($OPTIND - 1)) - - -## main - -isabelle_admin_build jars || exit $? - -if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then - echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" - - show_settings "" - echo -fi - -declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)" - -. "$ISABELLE_HOME/lib/scripts/timestart.bash" - -isabelle java "${JAVA_ARGS[@]}" isabelle.Build \ - "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \ - "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ - "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \ - "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \ - "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSION_GROUPS[@]}" $'\n' \ - "${EXCLUDE_SESSIONS[@]}" $'\n' "$@" -RC="$?" - -if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then - echo -n "Finished at "; date -fi - -. "$ISABELLE_HOME/lib/scripts/timestop.bash" -echo "$TIMES_REPORT" - -exit "$RC" +exec isabelle java "${JAVA_ARGS[@]}" isabelle.Build "$@" diff -r b5783412bfed -r 0c837beeb5e7 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Mar 10 17:30:04 2016 +0100 +++ b/src/Pure/Tools/build.scala Thu Mar 10 22:09:44 2016 +0100 @@ -1027,29 +1027,113 @@ def main(args: Array[String]) { Command_Line.tool { - args.toList match { - case - Properties.Value.Boolean(requirements) :: - Properties.Value.Boolean(all_sessions) :: - Properties.Value.Boolean(build_heap) :: - Properties.Value.Boolean(clean_build) :: - Properties.Value.Int(max_jobs) :: - Properties.Value.Boolean(list_files) :: - Properties.Value.Boolean(no_build) :: - Properties.Value.Boolean(system_mode) :: - Properties.Value.Boolean(verbose) :: - Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords, - build_options, exclude_session_groups, exclude_sessions, sessions) => - val options = (Options.init() /: build_options)(_ + _) - val progress = new Console_Progress(verbose) - progress.interrupt_handler { - build(options, progress, requirements, all_sessions, build_heap, clean_build, - dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), exclude_session_groups, - session_groups, max_jobs, list_files, check_keywords.toSet, no_build, system_mode, - verbose, exclude_sessions, sessions) - } - case _ => error("Bad arguments:\n" + cat_lines(args)) + def show_settings(): String = + cat_lines(List( + "ISABELLE_BUILD_OPTIONS=" + + quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")), + "", + "ISABELLE_BUILD_JAVA_OPTIONS=" + + quote(Isabelle_System.getenv("ISABELLE_BUILD_JAVA_OPTIONS")) + + "", + "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")), + "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")), + "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")), + "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS")))) + + val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) + + var select_dirs: List[Path] = Nil + var requirements = false + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var build_heap = false + var clean_build = false + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var max_jobs = 1 + var check_keywords: Set[String] = Set.empty + var list_files = false + var no_build = false + var options = (Options.init() /: build_options)(_ + _) + var system_mode = false + var verbose = false + var exclude_sessions: List[String] = Nil + + val getopts = Getopts(""" +Usage: isabelle build [OPTIONS] [SESSIONS ...] + + Options are: + -D DIR include session directory and select its sessions + -R operate on requirements of selected sessions + -X NAME exclude sessions from group NAME and all descendants + -a select all sessions + -b build heap images + -c clean build + -d DIR include session directory + -g NAME select session group NAME + -j INT maximum number of parallel jobs (default 1) + -k KEYWORD check theory sources for conflicts with proposed keywords + -l list session source files + -n no build -- test dependencies only + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -s system build mode: produce output in ISABELLE_HOME + -v verbose + -x NAME exclude session NAME and all descendants + + Build and manage Isabelle sessions, depending on implicit +""" + Library.prefix_lines(" ", show_settings()), + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "R" -> (_ => requirements = true), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "b" -> (_ => build_heap = true), + "c" -> (_ => clean_build = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)), + "k:" -> (arg => check_keywords = check_keywords + arg), + "l" -> (_ => list_files = true), + "n" -> (_ => no_build = true), + "o:" -> (arg => options = options + arg), + "s" -> (_ => system_mode = true), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + + val sessions = getopts(args) + + val progress = new Console_Progress(verbose) + val start_time = Time.now() + val show_timing = !no_build && verbose + + if (show_timing) { + progress.echo( + Library.trim_line( + Isabelle_System.bash( + """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out)) + progress.echo(show_settings()) } + + val results = + progress.interrupt_handler { + build_results(options, progress, requirements, all_sessions, build_heap, clean_build, + dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files, + check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions) + } + + if (show_timing) { + val elapsed_time = Time.now() - start_time + + progress.echo( + Library.trim_line( + Isabelle_System.bash("""echo "Finished at "; date""").out)) + + val total_timing = + (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _). + copy(elapsed = elapsed_time) + progress.echo(total_timing.message_resources) + } + + results.rc } } diff -r b5783412bfed -r 0c837beeb5e7 src/Pure/library.scala --- a/src/Pure/library.scala Thu Mar 10 17:30:04 2016 +0100 +++ b/src/Pure/library.scala Thu Mar 10 22:09:44 2016 +0100 @@ -97,6 +97,10 @@ def split_lines(str: String): List[String] = space_explode('\n', str) + def prefix_lines(prfx: String, str: String): String = + if (str == "") str + else cat_lines(split_lines(str).map(s => prfx + s)) + def first_line(source: CharSequence): String = { val lines = separated_chunks(_ == '\n', source)