# HG changeset patch # User wenzelm # Date 1357676211 -3600 # Node ID 20126dd9772c973118879a6878acfd9e6c66f1e7 # Parent 5a9964f7a6915cfa8a144fc9acc9fddec562ff9b include timing properties in log; general Properties.parse operations; tuned signature; diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/General/properties.scala --- a/src/Pure/General/properties.scala Tue Jan 08 19:02:12 2013 +0100 +++ b/src/Pure/General/properties.scala Tue Jan 08 21:16:51 2013 +0100 @@ -102,5 +102,34 @@ case Some((_, value)) => Value.Double.unapply(value) } } + + + /* concrete syntax -- similar to ML */ + + private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]" + + private object Parser extends Parse.Parser + { + def prop: Parser[Entry] = + keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^ + { case _ ~ x ~ _ ~ y ~ _ => (x, y) } + def props: Parser[T] = + keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]") + } + + def parse(text: java.lang.String): Properties.T = + { + Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match { + case Parser.Success(result, _) => result + case bad => error(bad.toString) + } + } + + def parse_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] = + for (line <- lines if line.startsWith(prefix)) + yield parse(line.substring(prefix.length)) + + def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] = + lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length))) } diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/General/timing.ML --- a/src/Pure/General/timing.ML Tue Jan 08 19:02:12 2013 +0100 +++ b/src/Pure/General/timing.ML Tue Jan 08 21:16:51 2013 +0100 @@ -21,6 +21,7 @@ val result: start -> timing val timing: ('a -> 'b) -> 'a -> timing * 'b val is_relevant: timing -> bool + val properties: timing -> Properties.T val message: timing -> string end @@ -66,6 +67,17 @@ in (result start, y) end; +(* properties *) + +fun property name time = + [(name, Time.toString time)] handle Time.Time => []; + +fun properties {elapsed, cpu, gc} = + property "time_elapsed" elapsed @ + property "time_cpu" cpu @ + property "time_GC" gc; + + (* timing messages *) val min_time = Time.fromMilliseconds 1; diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Tue Jan 08 19:02:12 2013 +0100 +++ b/src/Pure/ML/ml_statistics.scala Tue Jan 08 21:16:51 2013 +0100 @@ -22,7 +22,7 @@ final case class Entry(time: Double, data: Map[String, Double]) def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats) - def apply(log: Path): ML_Statistics = apply(read_log(log)) + def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats) val empty = apply(Nil) @@ -50,37 +50,6 @@ val standard_fields = List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields) - - - /* read properties from build log */ - - private val line_prefix = "\fML_statistics = " - - private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]" - - private object Parser extends Parse.Parser - { - private def stat: Parser[(String, String)] = - keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^ - { case _ ~ x ~ _ ~ y ~ _ => (x, y) } - private def stats: Parser[Properties.T] = - keyword("[") ~> repsep(stat, keyword(",")) <~ keyword("]") - - def parse_stats(s: String): Properties.T = - { - parse_all(stats, Token.reader(syntax.scan(s))) match { - case Success(result, _) => result - case bad => error(bad.toString) - } - } - } - - def read_log(log: Path): List[Properties.T] = - for { - line <- split_lines(File.read_gzip(log)) - if line.startsWith(line_prefix) - stats = line.substring(line_prefix.length) - } yield Parser.parse_stats(stats) } final class ML_Statistics private(val stats: List[Properties.T]) diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/System/session.ML --- a/src/Pure/System/session.ML Tue Jan 08 19:02:12 2013 +0100 +++ b/src/Pure/System/session.ML Tue Jan 08 21:16:51 2013 +0100 @@ -86,19 +86,25 @@ (* use_dir *) -fun with_timing _ false f x = f x - | with_timing item true f x = - let - val start = Timing.start (); - val y = f x; - val timing = Timing.result start; - val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) - |> Real.fmt (StringCvt.FIX (SOME 2)); - val _ = - Output.physical_stderr ("Timing " ^ item ^ " (" ^ - string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ - Timing.message timing ^ ", factor " ^ factor ^ ")\n"); - in y end; +fun with_timing name verbose f x = + let + val start = Timing.start (); + val y = f x; + val timing = Timing.result start; + + val threads = string_of_int (Multithreading.max_threads_value ()); + val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) + |> Real.fmt (StringCvt.FIX (SOME 2)); + + val _ = + writeln ("\fTiming = " ^ ML_Syntax.print_properties + ([("threads", threads)] @ Timing.properties timing @ [("factor", factor)])); + val _ = + if verbose then + Output.physical_stderr ("Timing " ^ name ^ " (" ^ + threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") + else (); + in y end; fun get_rpath rpath = (if rpath = "" then () else diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Tue Jan 08 19:02:12 2013 +0100 +++ b/src/Pure/Tools/build.ML Tue Jan 08 21:16:51 2013 +0100 @@ -21,8 +21,7 @@ fun protocol_message props output = (case ML_statistics props output of - SOME stats => - writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats) + SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats) | NONE => raise Fail "Undefined Output.protocol_message"); diff -r 5a9964f7a691 -r 20126dd9772c src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Jan 08 19:02:12 2013 +0100 +++ b/src/Pure/Tools/build.scala Tue Jan 08 21:16:51 2013 +0100 @@ -509,7 +509,7 @@ } - /* log files and corresponding heaps */ + /* log files */ private val LOG = Path.explode("log") private def log(name: String): Path = LOG + Path.basic(name) @@ -517,6 +517,19 @@ private val SESSION_PARENT_PATH = "\fSession.parent_path = " + sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T) + + def parse_log(text: String): Log_Info = + { + val lines = split_lines(text) + val stats = Properties.parse_lines("\fML_statistics = ", lines) + val timing = Properties.find_parse_line("\fTiming = ", lines) getOrElse Nil + Log_Info(stats, timing) + } + + + /* sources and heaps */ + private def sources_stamp(digests: List[SHA1.Digest]): String = digests.map(_.toString).sorted.mkString("sources: ", " ", "")