# HG changeset patch
# User wenzelm
# Date 1476019698 -7200
# Node ID 8094eaa38d4b8fa2716b8918b05147c1ff5b6ead
# Parent  0996fab2ec03c6983f99f3b5caa3a8ccfecb229e
inline session ML statistics into main build log;
tuned;

diff -r 0996fab2ec03 -r 8094eaa38d4b src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala	Sun Oct 09 14:19:46 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Sun Oct 09 15:28:18 2016 +0200
@@ -17,7 +17,7 @@
   /* log files */
 
   val BUILD_HISTORY = "build_history"
-  val META_INFO = "\fmeta_info = "
+  val META_INFO_MARKER = "\fmeta_info = "
 
   def log_date(date: Date): String =
     String.format(Locale.ROOT, "%s.%05d",
@@ -256,10 +256,12 @@
       val res = other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose)
       val build_end = Date.now()
 
+
+      /* output log */
+
       val log_path =
         other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) +
           Path.explode(log_name(build_history_date, ml_platform, "M" + threads))
-      Isabelle_System.mkdirs(log_path.dir)
 
       val meta_info =
         List(Build_Log.Field.build_engine -> BUILD_HISTORY,
@@ -268,11 +270,29 @@
           Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end),
           Build_Log.Field.isabelle_version -> isabelle_version)
 
+      val ml_statistics =
+        Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info().
+          finished_sessions.flatMap(session_name =>
+            {
+              val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
+              if (session_log.is_file) {
+                Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
+                  ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
+              }
+              else Nil
+            })
+
+      Isabelle_System.mkdirs(log_path.dir)
       File.write_gzip(log_path,
-        Build_Log.Log_File.print_props(META_INFO, meta_info) + "\n" + res.out)
+        cat_lines(
+          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
+          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))))
 
       Output.writeln(log_path.implode, stdout = true)
 
+
+      /* next build */
+
       if (multicore_base && first_build && isabelle_output_log.is_dir)
         other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
 
diff -r 0996fab2ec03 -r 8094eaa38d4b src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Sun Oct 09 14:19:46 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Sun Oct 09 15:28:18 2016 +0200
@@ -136,8 +136,8 @@
 
     /* inlined content */
 
-    def print_props(prefix: String, props: Properties.T): String =
-      prefix + YXML.string_of_body(XML.Encode.properties(props))
+    def print_props(marker: String, props: Properties.T): String =
+      marker + YXML.string_of_body(XML.Encode.properties(props))
   }
 
   class Log_File private(val name: String, val lines: List[String])
@@ -191,14 +191,14 @@
     def parse_props(text: String): Properties.T =
       xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
 
-    def filter_props(prefix: String): List[Properties.T] =
-      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s)
+    def filter_props(marker: String): List[Properties.T] =
+      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
 
-    def find_line(prefix: String): Option[String] =
-      find(Library.try_unprefix(prefix, _))
+    def find_line(marker: String): Option[String] =
+      find(Library.try_unprefix(marker, _))
 
-    def find_props(prefix: String): Option[Properties.T] =
-      find_line(prefix).map(parse_props(_))
+    def find_props(marker: String): Option[Properties.T] =
+      find_line(marker).map(parse_props(_))
 
 
     /* parse various formats */
@@ -300,8 +300,8 @@
     }
 
     log_file.lines match {
-      case line :: _ if line.startsWith(Build_History.META_INFO) =>
-        Meta_Info(log_file.find_props(Build_History.META_INFO).get,
+      case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) =>
+        Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get,
           log_file.get_settings(Settings.all_settings))
 
       case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
@@ -337,7 +337,10 @@
 
 
 
-  /** build info: produced by isabelle build **/
+  /** build info: produced by isabelle build or build_history **/
+
+  val ML_STATISTICS_MARKER = "\fML_statistics = "
+  val SESSION_NAME = "session_name"
 
   object Session_Status extends Enumeration
   {
@@ -353,6 +356,7 @@
     threads: Option[Int],
     timing: Timing,
     ml_timing: Timing,
+    ml_statistics: List[Properties.T],
     status: Session_Status.Value)
   {
     def finished: Boolean = status == Session_Status.FINISHED
@@ -369,6 +373,7 @@
         case None => x
       }
 
+    def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
     def finished(name: String): Boolean = get_default(name, _.finished, false)
     def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
     def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
@@ -405,9 +410,11 @@
     var started = Set.empty[String]
     var failed = Set.empty[String]
     var cancelled = Set.empty[String]
+    var ml_statistics = Map.empty[String, List[Properties.T]]
+
     def all_sessions: Set[String] =
-      chapter.keySet ++ groups.keySet ++ threads.keySet ++
-      timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
+      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++
+      ml_timing.keySet ++ failed ++ cancelled ++ started ++ ml_statistics.keySet
 
 
     for (line <- log_file.lines) {
@@ -415,21 +422,26 @@
         case Session_No_Groups(Chapter_Name(chapt, name)) =>
           chapter += (name -> chapt)
           groups += (name -> Nil)
+
         case Session_Groups(Chapter_Name(chapt, name), grps) =>
           chapter += (name -> chapt)
           groups += (name -> Word.explode(grps))
+
         case Session_Started(name) =>
           started += name
+
         case Session_Finished1(name,
             Value.Int(e1), Value.Int(e2), Value.Int(e3),
             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
           val elapsed = Time.hms(e1, e2, e3)
           val cpu = Time.hms(c1, c2, c3)
           timing += (name -> Timing(elapsed, cpu, Time.zero))
+
         case Session_Finished2(name,
             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
           val elapsed = Time.hms(e1, e2, e3)
           timing += (name -> Timing(elapsed, Time.zero, Time.zero))
+
         case Session_Timing(name,
             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
           val elapsed = Time.seconds(e)
@@ -437,6 +449,15 @@
           val gc = Time.seconds(g)
           ml_timing += (name -> Timing(elapsed, cpu, gc))
           threads += (name -> t)
+
+        case _ if line.startsWith(ML_STATISTICS_MARKER) =>
+          val (name, props) =
+            Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
+              case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
+              case _ => log_file.err("malformed ML_statistics " + quote(line))
+            }
+          ml_statistics = ml_statistics + (name -> (props :: ml_statistics.getOrElse(name, Nil)))
+
         case _ =>
       }
     }
@@ -458,6 +479,7 @@
               threads.get(name),
               timing.getOrElse(name, Timing.zero),
               ml_timing.getOrElse(name, Timing.zero),
+              ml_statistics.getOrElse(name, Nil).reverse,
               status)
           (name -> entry)
         }):_*)
@@ -494,7 +516,7 @@
     val command_timings_ =
       if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
     val ml_statistics_ =
-      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
+      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
     val task_statistics_ =
       if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil