inline session ML statistics into main build log;
authorwenzelm
Sun Oct 09 15:28:18 2016 +0200 (2016-10-09)
changeset 641198094eaa38d4b
parent 64118 0996fab2ec03
child 64120 6c5039016321
inline session ML statistics into main build log;
tuned;
src/Pure/Tools/build_history.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_history.scala	Sun Oct 09 14:19:46 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_history.scala	Sun Oct 09 15:28:18 2016 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    /* log files */
     1.5  
     1.6    val BUILD_HISTORY = "build_history"
     1.7 -  val META_INFO = "\fmeta_info = "
     1.8 +  val META_INFO_MARKER = "\fmeta_info = "
     1.9  
    1.10    def log_date(date: Date): String =
    1.11      String.format(Locale.ROOT, "%s.%05d",
    1.12 @@ -256,10 +256,12 @@
    1.13        val res = other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose)
    1.14        val build_end = Date.now()
    1.15  
    1.16 +
    1.17 +      /* output log */
    1.18 +
    1.19        val log_path =
    1.20          other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) +
    1.21            Path.explode(log_name(build_history_date, ml_platform, "M" + threads))
    1.22 -      Isabelle_System.mkdirs(log_path.dir)
    1.23  
    1.24        val meta_info =
    1.25          List(Build_Log.Field.build_engine -> BUILD_HISTORY,
    1.26 @@ -268,11 +270,29 @@
    1.27            Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end),
    1.28            Build_Log.Field.isabelle_version -> isabelle_version)
    1.29  
    1.30 +      val ml_statistics =
    1.31 +        Build_Log.Log_File(log_path.base.implode, res.out_lines).parse_build_info().
    1.32 +          finished_sessions.flatMap(session_name =>
    1.33 +            {
    1.34 +              val session_log = isabelle_output_log + Path.explode(session_name).ext("gz")
    1.35 +              if (session_log.is_file) {
    1.36 +                Build_Log.Log_File(session_log).parse_session_info(ml_statistics = true).
    1.37 +                  ml_statistics.map(props => (Build_Log.SESSION_NAME -> session_name) :: props)
    1.38 +              }
    1.39 +              else Nil
    1.40 +            })
    1.41 +
    1.42 +      Isabelle_System.mkdirs(log_path.dir)
    1.43        File.write_gzip(log_path,
    1.44 -        Build_Log.Log_File.print_props(META_INFO, meta_info) + "\n" + res.out)
    1.45 +        cat_lines(
    1.46 +          Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines :::
    1.47 +          ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))))
    1.48  
    1.49        Output.writeln(log_path.implode, stdout = true)
    1.50  
    1.51 +
    1.52 +      /* next build */
    1.53 +
    1.54        if (multicore_base && first_build && isabelle_output_log.is_dir)
    1.55          other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
    1.56  
     2.1 --- a/src/Pure/Tools/build_log.scala	Sun Oct 09 14:19:46 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Sun Oct 09 15:28:18 2016 +0200
     2.3 @@ -136,8 +136,8 @@
     2.4  
     2.5      /* inlined content */
     2.6  
     2.7 -    def print_props(prefix: String, props: Properties.T): String =
     2.8 -      prefix + YXML.string_of_body(XML.Encode.properties(props))
     2.9 +    def print_props(marker: String, props: Properties.T): String =
    2.10 +      marker + YXML.string_of_body(XML.Encode.properties(props))
    2.11    }
    2.12  
    2.13    class Log_File private(val name: String, val lines: List[String])
    2.14 @@ -191,14 +191,14 @@
    2.15      def parse_props(text: String): Properties.T =
    2.16        xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
    2.17  
    2.18 -    def filter_props(prefix: String): List[Properties.T] =
    2.19 -      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s)
    2.20 +    def filter_props(marker: String): List[Properties.T] =
    2.21 +      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield parse_props(s)
    2.22  
    2.23 -    def find_line(prefix: String): Option[String] =
    2.24 -      find(Library.try_unprefix(prefix, _))
    2.25 +    def find_line(marker: String): Option[String] =
    2.26 +      find(Library.try_unprefix(marker, _))
    2.27  
    2.28 -    def find_props(prefix: String): Option[Properties.T] =
    2.29 -      find_line(prefix).map(parse_props(_))
    2.30 +    def find_props(marker: String): Option[Properties.T] =
    2.31 +      find_line(marker).map(parse_props(_))
    2.32  
    2.33  
    2.34      /* parse various formats */
    2.35 @@ -300,8 +300,8 @@
    2.36      }
    2.37  
    2.38      log_file.lines match {
    2.39 -      case line :: _ if line.startsWith(Build_History.META_INFO) =>
    2.40 -        Meta_Info(log_file.find_props(Build_History.META_INFO).get,
    2.41 +      case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) =>
    2.42 +        Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get,
    2.43            log_file.get_settings(Settings.all_settings))
    2.44  
    2.45        case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
    2.46 @@ -337,7 +337,10 @@
    2.47  
    2.48  
    2.49  
    2.50 -  /** build info: produced by isabelle build **/
    2.51 +  /** build info: produced by isabelle build or build_history **/
    2.52 +
    2.53 +  val ML_STATISTICS_MARKER = "\fML_statistics = "
    2.54 +  val SESSION_NAME = "session_name"
    2.55  
    2.56    object Session_Status extends Enumeration
    2.57    {
    2.58 @@ -353,6 +356,7 @@
    2.59      threads: Option[Int],
    2.60      timing: Timing,
    2.61      ml_timing: Timing,
    2.62 +    ml_statistics: List[Properties.T],
    2.63      status: Session_Status.Value)
    2.64    {
    2.65      def finished: Boolean = status == Session_Status.FINISHED
    2.66 @@ -369,6 +373,7 @@
    2.67          case None => x
    2.68        }
    2.69  
    2.70 +    def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
    2.71      def finished(name: String): Boolean = get_default(name, _.finished, false)
    2.72      def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
    2.73      def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
    2.74 @@ -405,9 +410,11 @@
    2.75      var started = Set.empty[String]
    2.76      var failed = Set.empty[String]
    2.77      var cancelled = Set.empty[String]
    2.78 +    var ml_statistics = Map.empty[String, List[Properties.T]]
    2.79 +
    2.80      def all_sessions: Set[String] =
    2.81 -      chapter.keySet ++ groups.keySet ++ threads.keySet ++
    2.82 -      timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
    2.83 +      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++
    2.84 +      ml_timing.keySet ++ failed ++ cancelled ++ started ++ ml_statistics.keySet
    2.85  
    2.86  
    2.87      for (line <- log_file.lines) {
    2.88 @@ -415,21 +422,26 @@
    2.89          case Session_No_Groups(Chapter_Name(chapt, name)) =>
    2.90            chapter += (name -> chapt)
    2.91            groups += (name -> Nil)
    2.92 +
    2.93          case Session_Groups(Chapter_Name(chapt, name), grps) =>
    2.94            chapter += (name -> chapt)
    2.95            groups += (name -> Word.explode(grps))
    2.96 +
    2.97          case Session_Started(name) =>
    2.98            started += name
    2.99 +
   2.100          case Session_Finished1(name,
   2.101              Value.Int(e1), Value.Int(e2), Value.Int(e3),
   2.102              Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   2.103            val elapsed = Time.hms(e1, e2, e3)
   2.104            val cpu = Time.hms(c1, c2, c3)
   2.105            timing += (name -> Timing(elapsed, cpu, Time.zero))
   2.106 +
   2.107          case Session_Finished2(name,
   2.108              Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   2.109            val elapsed = Time.hms(e1, e2, e3)
   2.110            timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   2.111 +
   2.112          case Session_Timing(name,
   2.113              Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   2.114            val elapsed = Time.seconds(e)
   2.115 @@ -437,6 +449,15 @@
   2.116            val gc = Time.seconds(g)
   2.117            ml_timing += (name -> Timing(elapsed, cpu, gc))
   2.118            threads += (name -> t)
   2.119 +
   2.120 +        case _ if line.startsWith(ML_STATISTICS_MARKER) =>
   2.121 +          val (name, props) =
   2.122 +            Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
   2.123 +              case Some((SESSION_NAME, session_name) :: props) => (session_name, props)
   2.124 +              case _ => log_file.err("malformed ML_statistics " + quote(line))
   2.125 +            }
   2.126 +          ml_statistics = ml_statistics + (name -> (props :: ml_statistics.getOrElse(name, Nil)))
   2.127 +
   2.128          case _ =>
   2.129        }
   2.130      }
   2.131 @@ -458,6 +479,7 @@
   2.132                threads.get(name),
   2.133                timing.getOrElse(name, Timing.zero),
   2.134                ml_timing.getOrElse(name, Timing.zero),
   2.135 +              ml_statistics.getOrElse(name, Nil).reverse,
   2.136                status)
   2.137            (name -> entry)
   2.138          }):_*)
   2.139 @@ -494,7 +516,7 @@
   2.140      val command_timings_ =
   2.141        if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   2.142      val ml_statistics_ =
   2.143 -      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   2.144 +      if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil
   2.145      val task_statistics_ =
   2.146        if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   2.147