src/Pure/Tools/build_log.scala
author wenzelm
Wed Oct 05 14:15:54 2016 +0200 (2016-10-05)
changeset 64054 1fc9ab31720d
parent 64053 7ece2e14fd6c
child 64061 1bbea2b55d22
permissions -rw-r--r--
clarified modules;
     1 /*  Title:      Pure/Tools/build_log.scala
     2     Author:     Makarius
     3 
     4 Build log parsing for historic versions, back to "build_history_base".
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.mutable
    11 import scala.util.matching.Regex
    12 
    13 
    14 object Build_Log
    15 {
    16   /* inlined properties (YXML) */
    17 
    18   object Props
    19   {
    20     def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props))
    21     def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    22 
    23     def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    24       for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    25 
    26     def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    27       lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    28   }
    29 
    30 
    31   /* session log: produced by "isabelle build" */
    32 
    33   sealed case class Session_Info(
    34     session_name: String,
    35     session_timing: Properties.T,
    36     command_timings: List[Properties.T],
    37     ml_statistics: List[Properties.T],
    38     task_statistics: List[Properties.T])
    39 
    40   val SESSION_NAME = "\fSession.name = "
    41 
    42   def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    43   {
    44     val xml_cache = new XML.Cache()
    45     def parse_lines(prfx: String): List[Properties.T] =
    46       Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    47 
    48     val session_name =
    49       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
    50         case None => name0
    51         case Some(name) if name0 == "" || name0 == name => name
    52         case Some(name) =>
    53           error("Session log for " + quote(name0) + " is actually from " + quote(name))
    54       }
    55     val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    56     val command_timings = parse_lines("\fcommand_timing = ")
    57     val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    58     val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    59 
    60     Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    61   }
    62 
    63 
    64   /* main log: produced by isatest, afp-test, jenkins etc. */
    65 
    66   sealed case class Info(
    67     ml_options: List[(String, String)],
    68     finished: Map[String, Timing],
    69     timing: Map[String, Timing],
    70     threads: Map[String, Int])
    71   {
    72     val sessions: Set[String] = finished.keySet ++ timing.keySet
    73 
    74     override def toString: String =
    75       sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")")
    76   }
    77 
    78   private val Session_Finished1 =
    79     new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
    80   private val Session_Finished2 =
    81     new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
    82   private val Session_Timing =
    83     new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
    84 
    85   private object ML_Option
    86   {
    87     def unapply(s: String): Option[(String, String)] =
    88       s.indexOf('=') match {
    89         case -1 => None
    90         case i =>
    91           val a = s.substring(0, i)
    92           Library.try_unquote(s.substring(i + 1)) match {
    93             case Some(b) if Build.ml_options.contains(a) => Some((a, b))
    94             case _ => None
    95           }
    96       }
    97   }
    98 
    99   def parse_info(text: String): Info =
   100   {
   101     val ml_options = new mutable.ListBuffer[(String, String)]
   102     var finished = Map.empty[String, Timing]
   103     var timing = Map.empty[String, Timing]
   104     var threads = Map.empty[String, Int]
   105 
   106     for (line <- split_lines(text)) {
   107       line match {
   108         case Session_Finished1(name,
   109             Value.Int(e1), Value.Int(e2), Value.Int(e3),
   110             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   111           val elapsed = Time.hms(e1, e2, e3)
   112           val cpu = Time.hms(c1, c2, c3)
   113           finished += (name -> Timing(elapsed, cpu, Time.zero))
   114         case Session_Finished2(name,
   115             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   116           val elapsed = Time.hms(e1, e2, e3)
   117           finished += (name -> Timing(elapsed, Time.zero, Time.zero))
   118         case Session_Timing(name,
   119             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   120           val elapsed = Time.seconds(e)
   121           val cpu = Time.seconds(c)
   122           val gc = Time.seconds(g)
   123           timing += (name -> Timing(elapsed, cpu, gc))
   124           threads += (name -> t)
   125         case ML_Option(a, b) => ml_options += (a -> b)
   126         case _ =>
   127       }
   128     }
   129 
   130     Info(ml_options.toList, finished, timing, threads)
   131   }
   132 }