include timing properties in log; build_history_base
authorwenzelm
Tue Jan 08 21:16:51 2013 +0100 (2013-01-08)
changeset 5077720126dd9772c
parent 50776 5a9964f7a691
child 50778 15dc91cf4750
include timing properties in log;
general Properties.parse operations;
tuned signature;
src/Pure/General/properties.scala
src/Pure/General/timing.ML
src/Pure/ML/ml_statistics.scala
src/Pure/System/session.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/General/properties.scala	Tue Jan 08 19:02:12 2013 +0100
     1.2 +++ b/src/Pure/General/properties.scala	Tue Jan 08 21:16:51 2013 +0100
     1.3 @@ -102,5 +102,34 @@
     1.4          case Some((_, value)) => Value.Double.unapply(value)
     1.5        }
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* concrete syntax -- similar to ML */
    1.10 +
    1.11 +  private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
    1.12 +
    1.13 +  private object Parser extends Parse.Parser
    1.14 +  {
    1.15 +    def prop: Parser[Entry] =
    1.16 +      keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
    1.17 +      { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
    1.18 +    def props: Parser[T] =
    1.19 +      keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]")
    1.20 +  }
    1.21 +
    1.22 +  def parse(text: java.lang.String): Properties.T =
    1.23 +  {
    1.24 +    Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match {
    1.25 +      case Parser.Success(result, _) => result
    1.26 +      case bad => error(bad.toString)
    1.27 +    }
    1.28 +  }
    1.29 +
    1.30 +  def parse_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] =
    1.31 +    for (line <- lines if line.startsWith(prefix))
    1.32 +      yield parse(line.substring(prefix.length))
    1.33 +
    1.34 +  def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] =
    1.35 +    lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    1.36  }
    1.37  
     2.1 --- a/src/Pure/General/timing.ML	Tue Jan 08 19:02:12 2013 +0100
     2.2 +++ b/src/Pure/General/timing.ML	Tue Jan 08 21:16:51 2013 +0100
     2.3 @@ -21,6 +21,7 @@
     2.4    val result: start -> timing
     2.5    val timing: ('a -> 'b) -> 'a -> timing * 'b
     2.6    val is_relevant: timing -> bool
     2.7 +  val properties: timing -> Properties.T
     2.8    val message: timing -> string
     2.9  end
    2.10  
    2.11 @@ -66,6 +67,17 @@
    2.12    in (result start, y) end;
    2.13  
    2.14  
    2.15 +(* properties *)
    2.16 +
    2.17 +fun property name time =
    2.18 +  [(name, Time.toString time)] handle Time.Time => [];
    2.19 +
    2.20 +fun properties {elapsed, cpu, gc} =
    2.21 +  property "time_elapsed" elapsed @
    2.22 +  property "time_cpu" cpu @
    2.23 +  property "time_GC" gc;
    2.24 +
    2.25 +
    2.26  (* timing messages *)
    2.27  
    2.28  val min_time = Time.fromMilliseconds 1;
     3.1 --- a/src/Pure/ML/ml_statistics.scala	Tue Jan 08 19:02:12 2013 +0100
     3.2 +++ b/src/Pure/ML/ml_statistics.scala	Tue Jan 08 21:16:51 2013 +0100
     3.3 @@ -22,7 +22,7 @@
     3.4    final case class Entry(time: Double, data: Map[String, Double])
     3.5  
     3.6    def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
     3.7 -  def apply(log: Path): ML_Statistics = apply(read_log(log))
     3.8 +  def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
     3.9  
    3.10    val empty = apply(Nil)
    3.11  
    3.12 @@ -50,37 +50,6 @@
    3.13  
    3.14    val standard_fields =
    3.15      List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
    3.16 -
    3.17 -
    3.18 -  /* read properties from build log */
    3.19 -
    3.20 -  private val line_prefix = "\fML_statistics = "
    3.21 -
    3.22 -  private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]"
    3.23 -
    3.24 -  private object Parser extends Parse.Parser
    3.25 -  {
    3.26 -    private def stat: Parser[(String, String)] =
    3.27 -      keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^
    3.28 -      { case _ ~ x ~ _ ~ y ~ _ => (x, y) }
    3.29 -    private def stats: Parser[Properties.T] =
    3.30 -      keyword("[") ~> repsep(stat, keyword(",")) <~ keyword("]")
    3.31 -
    3.32 -    def parse_stats(s: String): Properties.T =
    3.33 -    {
    3.34 -      parse_all(stats, Token.reader(syntax.scan(s))) match {
    3.35 -        case Success(result, _) => result
    3.36 -        case bad => error(bad.toString)
    3.37 -      }
    3.38 -    }
    3.39 -  }
    3.40 -
    3.41 -  def read_log(log: Path): List[Properties.T] =
    3.42 -    for {
    3.43 -      line <- split_lines(File.read_gzip(log))
    3.44 -      if line.startsWith(line_prefix)
    3.45 -      stats = line.substring(line_prefix.length)
    3.46 -    } yield Parser.parse_stats(stats)
    3.47  }
    3.48  
    3.49  final class ML_Statistics private(val stats: List[Properties.T])
     4.1 --- a/src/Pure/System/session.ML	Tue Jan 08 19:02:12 2013 +0100
     4.2 +++ b/src/Pure/System/session.ML	Tue Jan 08 21:16:51 2013 +0100
     4.3 @@ -86,19 +86,25 @@
     4.4  
     4.5  (* use_dir *)
     4.6  
     4.7 -fun with_timing _ false f x = f x
     4.8 -  | with_timing item true f x =
     4.9 -      let
    4.10 -        val start = Timing.start ();
    4.11 -        val y = f x;
    4.12 -        val timing = Timing.result start;
    4.13 -        val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    4.14 -          |> Real.fmt (StringCvt.FIX (SOME 2));
    4.15 -        val _ =
    4.16 -          Output.physical_stderr ("Timing " ^ item ^ " (" ^
    4.17 -            string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
    4.18 -            Timing.message timing ^ ", factor " ^ factor ^ ")\n");
    4.19 -      in y end;
    4.20 +fun with_timing name verbose f x =
    4.21 +  let
    4.22 +    val start = Timing.start ();
    4.23 +    val y = f x;
    4.24 +    val timing = Timing.result start;
    4.25 +
    4.26 +    val threads = string_of_int (Multithreading.max_threads_value ());
    4.27 +    val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    4.28 +      |> Real.fmt (StringCvt.FIX (SOME 2));
    4.29 +
    4.30 +    val _ =
    4.31 +      writeln ("\fTiming = " ^ ML_Syntax.print_properties
    4.32 +        ([("threads", threads)] @ Timing.properties timing @ [("factor", factor)]));
    4.33 +    val _ =
    4.34 +      if verbose then
    4.35 +        Output.physical_stderr ("Timing " ^ name ^ " (" ^
    4.36 +          threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
    4.37 +      else ();
    4.38 +  in y end;
    4.39  
    4.40  fun get_rpath rpath =
    4.41    (if rpath = "" then () else
     5.1 --- a/src/Pure/Tools/build.ML	Tue Jan 08 19:02:12 2013 +0100
     5.2 +++ b/src/Pure/Tools/build.ML	Tue Jan 08 21:16:51 2013 +0100
     5.3 @@ -21,8 +21,7 @@
     5.4  
     5.5  fun protocol_message props output =
     5.6    (case ML_statistics props output of
     5.7 -    SOME stats =>
     5.8 -      writeln ("\f" ^ #2 Markup.ML_statistics ^ " = " ^ ML_Syntax.print_properties stats)
     5.9 +    SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
    5.10    | NONE => raise Fail "Undefined Output.protocol_message");
    5.11  
    5.12  
     6.1 --- a/src/Pure/Tools/build.scala	Tue Jan 08 19:02:12 2013 +0100
     6.2 +++ b/src/Pure/Tools/build.scala	Tue Jan 08 21:16:51 2013 +0100
     6.3 @@ -509,7 +509,7 @@
     6.4    }
     6.5  
     6.6  
     6.7 -  /* log files and corresponding heaps */
     6.8 +  /* log files */
     6.9  
    6.10    private val LOG = Path.explode("log")
    6.11    private def log(name: String): Path = LOG + Path.basic(name)
    6.12 @@ -517,6 +517,19 @@
    6.13  
    6.14    private val SESSION_PARENT_PATH = "\fSession.parent_path = "
    6.15  
    6.16 +  sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
    6.17 +
    6.18 +  def parse_log(text: String): Log_Info =
    6.19 +  {
    6.20 +    val lines = split_lines(text)
    6.21 +    val stats = Properties.parse_lines("\fML_statistics = ", lines)
    6.22 +    val timing = Properties.find_parse_line("\fTiming = ", lines) getOrElse Nil
    6.23 +    Log_Info(stats, timing)
    6.24 +  }
    6.25 +
    6.26 +
    6.27 +  /* sources and heaps */
    6.28 +
    6.29    private def sources_stamp(digests: List[SHA1.Digest]): String =
    6.30      digests.map(_.toString).sorted.mkString("sources: ", " ", "")
    6.31