# HG changeset patch # User wenzelm # Date 1343119143 -7200 # Node ID 375e45df6fdfda595eb4b51e371ef4c7ed0384e8 # Parent 09710d6fc3d1ecbdafd5e45e0d364e67c192290c timing is command line options, not system option; diff -r 09710d6fc3d1 -r 375e45df6fdf etc/options --- a/etc/options Tue Jul 24 10:11:49 2012 +0200 +++ b/etc/options Tue Jul 24 10:39:03 2012 +0200 @@ -18,7 +18,5 @@ declare proofs : int = 0 declare quick_and_dirty : bool = false -declare timing : bool = false - declare condition : string = "" diff -r 09710d6fc3d1 -r 375e45df6fdf lib/Tools/build --- a/lib/Tools/build Tue Jul 24 10:11:49 2012 +0200 +++ b/lib/Tools/build Tue Jul 24 10:39:03 2012 +0200 @@ -22,6 +22,7 @@ echo " -l list sessions only" echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" echo " -s system build mode: produce output in ISABELLE_HOME" + echo " -t inner session timing" echo " -v verbose" echo echo " Build and manage Isabelle sessions, depending on implicit" @@ -54,12 +55,13 @@ MAX_JOBS=1 LIST_ONLY=false SYSTEM_MODE=false +TIMING=false VERBOSE=false declare -a MORE_DIRS=() eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" -while getopts "abd:j:lo:sv" OPT +while getopts "abd:j:lo:stv" OPT do case "$OPT" in a) @@ -84,6 +86,9 @@ s) SYSTEM_MODE="true" ;; + t) + TIMING="true" + ;; v) VERBOSE="true" ;; @@ -101,5 +106,5 @@ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } exec "$ISABELLE_TOOL" java isabelle.Build \ - "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \ - "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" + "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$TIMING" \ + "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" diff -r 09710d6fc3d1 -r 375e45df6fdf src/Pure/System/build.ML --- a/src/Pure/System/build.ML Tue Jul 24 10:11:49 2012 +0200 +++ b/src/Pure/System/build.ML Tue Jul 24 10:39:03 2012 +0200 @@ -12,9 +12,8 @@ structure Build: BUILD = struct -fun use_theories name options = +fun use_theories options = Thy_Info.use_thys - |> Session.with_timing name (Options.bool options "timing") |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs") |> Unsynchronized.setmp print_mode (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) @@ -27,11 +26,12 @@ fun build args_file = let - val (save, (options, (verbose, (browser_info, (parent, (name, (base_name, theories))))))) = + val (save, (options, (timing, (verbose, (browser_info, (parent, + (name, (base_name, theories)))))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in - pair bool (pair Options.decode (pair bool (pair string (pair string - (pair string (pair string ((list (pair Options.decode (list string)))))))))) + pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string + (pair string (pair string ((list (pair Options.decode (list string))))))))))) end; val _ = @@ -49,7 +49,7 @@ "" verbose; - val _ = List.app (uncurry (use_theories name)) theories; + val _ = List.app (uncurry (use_theories |> Session.with_timing name timing)) theories; val _ = Session.finish (); val _ = if save then () else quit (); diff -r 09710d6fc3d1 -r 375e45df6fdf src/Pure/System/build.scala --- a/src/Pure/System/build.scala Tue Jul 24 10:11:49 2012 +0200 +++ b/src/Pure/System/build.scala Tue Jul 24 10:39:03 2012 +0200 @@ -342,7 +342,7 @@ } private def start_job(name: String, info: Session.Info, output: Option[String], - options: Options, verbose: Boolean, browser_info: Path): Job = + options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job = { val parent = info.parent.getOrElse("") @@ -373,10 +373,10 @@ val args_xml = { import XML.Encode._ - pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string, - pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))( - (output.isDefined, (options, (verbose, (browser_info, (parent, - (name, (info.base_name, info.theories)))))))) + pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string, + pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))( + (output.isDefined, (options, (timing, (verbose, (browser_info, (parent, + (name, (info.base_name, info.theories))))))))) } new Job(cwd, env, script, YXML.string_of_body(args_xml)) } @@ -388,7 +388,7 @@ private def sleep(): Unit = Thread.sleep(500) def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int, - list_only: Boolean, system_mode: Boolean, verbose: Boolean, + list_only: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean, more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int = { val options = (Options.init() /: more_options)(_.define_simple(_)) @@ -458,7 +458,7 @@ Some(Isabelle_System.standard_path(output_dir + Path.basic(name))) else None echo((if (output.isDefined) "Building " else "Running ") + name + " ...") - val job = start_job(name, info, output, options, verbose, browser_info) + val job = start_job(name, info, output, options, timing, verbose, browser_info) loop(pending, running + (name -> job), results) } else { @@ -487,9 +487,10 @@ Properties.Value.Int(max_jobs) :: Properties.Value.Boolean(list_only) :: Properties.Value.Boolean(system_mode) :: + Properties.Value.Boolean(timing) :: Properties.Value.Boolean(verbose) :: Command_Line.Chunks(more_dirs, options, sessions) => - build(all_sessions, build_images, max_jobs, list_only, system_mode, + build(all_sessions, build_images, max_jobs, list_only, system_mode, timing, verbose, more_dirs.map(Path.explode), options, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) }