1.1 --- a/etc/options Tue Jul 24 10:11:49 2012 +0200
1.2 +++ b/etc/options Tue Jul 24 10:39:03 2012 +0200
1.3 @@ -18,7 +18,5 @@
1.4 declare proofs : int = 0
1.5 declare quick_and_dirty : bool = false
1.6
1.7 -declare timing : bool = false
1.8 -
1.9 declare condition : string = ""
1.10
2.1 --- a/lib/Tools/build Tue Jul 24 10:11:49 2012 +0200
2.2 +++ b/lib/Tools/build Tue Jul 24 10:39:03 2012 +0200
2.3 @@ -22,6 +22,7 @@
2.4 echo " -l list sessions only"
2.5 echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)"
2.6 echo " -s system build mode: produce output in ISABELLE_HOME"
2.7 + echo " -t inner session timing"
2.8 echo " -v verbose"
2.9 echo
2.10 echo " Build and manage Isabelle sessions, depending on implicit"
2.11 @@ -54,12 +55,13 @@
2.12 MAX_JOBS=1
2.13 LIST_ONLY=false
2.14 SYSTEM_MODE=false
2.15 +TIMING=false
2.16 VERBOSE=false
2.17
2.18 declare -a MORE_DIRS=()
2.19 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
2.20
2.21 -while getopts "abd:j:lo:sv" OPT
2.22 +while getopts "abd:j:lo:stv" OPT
2.23 do
2.24 case "$OPT" in
2.25 a)
2.26 @@ -84,6 +86,9 @@
2.27 s)
2.28 SYSTEM_MODE="true"
2.29 ;;
2.30 + t)
2.31 + TIMING="true"
2.32 + ;;
2.33 v)
2.34 VERBOSE="true"
2.35 ;;
2.36 @@ -101,5 +106,5 @@
2.37 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
2.38
2.39 exec "$ISABELLE_TOOL" java isabelle.Build \
2.40 - "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$VERBOSE" \
2.41 - "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
2.42 + "$ALL_SESSIONS" "$BUILD_IMAGES" "$MAX_JOBS" "$LIST_ONLY" "$SYSTEM_MODE" "$TIMING" \
2.43 + "$VERBOSE" "${MORE_DIRS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
3.1 --- a/src/Pure/System/build.ML Tue Jul 24 10:11:49 2012 +0200
3.2 +++ b/src/Pure/System/build.ML Tue Jul 24 10:39:03 2012 +0200
3.3 @@ -12,9 +12,8 @@
3.4 structure Build: BUILD =
3.5 struct
3.6
3.7 -fun use_theories name options =
3.8 +fun use_theories options =
3.9 Thy_Info.use_thys
3.10 - |> Session.with_timing name (Options.bool options "timing")
3.11 |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
3.12 |> Unsynchronized.setmp print_mode
3.13 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
3.14 @@ -27,11 +26,12 @@
3.15
3.16 fun build args_file =
3.17 let
3.18 - val (save, (options, (verbose, (browser_info, (parent, (name, (base_name, theories))))))) =
3.19 + val (save, (options, (timing, (verbose, (browser_info, (parent,
3.20 + (name, (base_name, theories)))))))) =
3.21 File.read (Path.explode args_file) |> YXML.parse_body |>
3.22 let open XML.Decode in
3.23 - pair bool (pair Options.decode (pair bool (pair string (pair string
3.24 - (pair string (pair string ((list (pair Options.decode (list string))))))))))
3.25 + pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
3.26 + (pair string (pair string ((list (pair Options.decode (list string)))))))))))
3.27 end;
3.28
3.29 val _ =
3.30 @@ -49,7 +49,7 @@
3.31 ""
3.32 verbose;
3.33
3.34 - val _ = List.app (uncurry (use_theories name)) theories;
3.35 + val _ = List.app (uncurry (use_theories |> Session.with_timing name timing)) theories;
3.36 val _ = Session.finish ();
3.37
3.38 val _ = if save then () else quit ();
4.1 --- a/src/Pure/System/build.scala Tue Jul 24 10:11:49 2012 +0200
4.2 +++ b/src/Pure/System/build.scala Tue Jul 24 10:39:03 2012 +0200
4.3 @@ -342,7 +342,7 @@
4.4 }
4.5
4.6 private def start_job(name: String, info: Session.Info, output: Option[String],
4.7 - options: Options, verbose: Boolean, browser_info: Path): Job =
4.8 + options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
4.9 {
4.10 val parent = info.parent.getOrElse("")
4.11
4.12 @@ -373,10 +373,10 @@
4.13 val args_xml =
4.14 {
4.15 import XML.Encode._
4.16 - pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
4.17 - pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
4.18 - (output.isDefined, (options, (verbose, (browser_info, (parent,
4.19 - (name, (info.base_name, info.theories))))))))
4.20 + pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
4.21 + pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
4.22 + (output.isDefined, (options, (timing, (verbose, (browser_info, (parent,
4.23 + (name, (info.base_name, info.theories)))))))))
4.24 }
4.25 new Job(cwd, env, script, YXML.string_of_body(args_xml))
4.26 }
4.27 @@ -388,7 +388,7 @@
4.28 private def sleep(): Unit = Thread.sleep(500)
4.29
4.30 def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
4.31 - list_only: Boolean, system_mode: Boolean, verbose: Boolean,
4.32 + list_only: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean,
4.33 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
4.34 {
4.35 val options = (Options.init() /: more_options)(_.define_simple(_))
4.36 @@ -458,7 +458,7 @@
4.37 Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
4.38 else None
4.39 echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
4.40 - val job = start_job(name, info, output, options, verbose, browser_info)
4.41 + val job = start_job(name, info, output, options, timing, verbose, browser_info)
4.42 loop(pending, running + (name -> job), results)
4.43 }
4.44 else {
4.45 @@ -487,9 +487,10 @@
4.46 Properties.Value.Int(max_jobs) ::
4.47 Properties.Value.Boolean(list_only) ::
4.48 Properties.Value.Boolean(system_mode) ::
4.49 + Properties.Value.Boolean(timing) ::
4.50 Properties.Value.Boolean(verbose) ::
4.51 Command_Line.Chunks(more_dirs, options, sessions) =>
4.52 - build(all_sessions, build_images, max_jobs, list_only, system_mode,
4.53 + build(all_sessions, build_images, max_jobs, list_only, system_mode, timing,
4.54 verbose, more_dirs.map(Path.explode), options, sessions)
4.55 case _ => error("Bad arguments:\n" + cat_lines(args))
4.56 }