timing is command line options, not system option;
authorwenzelm
Tue Jul 24 10:39:03 2012 +0200 (2012-07-24)
changeset 48459375e45df6fdf
parent 48458 09710d6fc3d1
child 48460 20170ae271a5
timing is command line options, not system option;
etc/options
lib/Tools/build
src/Pure/System/build.ML
src/Pure/System/build.scala
     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        }