src/Pure/Tools/build_log.scala
author wenzelm
Wed Oct 05 22:09:53 2016 +0200 (2016-10-05)
changeset 64061 1bbea2b55d22
parent 64054 1fc9ab31720d
child 64062 a7352cbde7d7
permissions -rw-r--r--
some support for header and data fields, notably from afp-test;
     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 java.time.ZonedDateTime
    11 import java.time.format.{DateTimeFormatter, DateTimeParseException}
    12 
    13 import scala.collection.mutable
    14 import scala.util.matching.Regex
    15 
    16 
    17 object Build_Log
    18 {
    19   /* inlined properties (YXML) */
    20 
    21   object Props
    22   {
    23     def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props))
    24     def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    25 
    26     def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    27       for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    28 
    29     def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    30       lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    31   }
    32 
    33 
    34   /* session log: produced by "isabelle build" */
    35 
    36   sealed case class Session_Info(
    37     session_name: String,
    38     session_timing: Properties.T,
    39     command_timings: List[Properties.T],
    40     ml_statistics: List[Properties.T],
    41     task_statistics: List[Properties.T])
    42 
    43   val SESSION_NAME = "\fSession.name = "
    44 
    45   def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    46   {
    47     val xml_cache = new XML.Cache()
    48     def parse_lines(prfx: String): List[Properties.T] =
    49       Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    50 
    51     val session_name =
    52       lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
    53         case None => name0
    54         case Some(name) if name0 == "" || name0 == name => name
    55         case Some(name) =>
    56           error("Session log for " + quote(name0) + " is actually from " + quote(name))
    57       }
    58     val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    59     val command_timings = parse_lines("\fcommand_timing = ")
    60     val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    61     val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    62 
    63     Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    64   }
    65 
    66 
    67   /* header and data fields */
    68 
    69   object Header_Kind extends Enumeration
    70   {
    71     val ISATEST = Value("isatest")
    72     val AFP_TEST = Value("afp-test")
    73     val JENKINS = Value("jenkins")
    74   }
    75 
    76   sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String])
    77 
    78   object Field
    79   {
    80     val build_host = "build_host"
    81     val build_start = "build_start"
    82     val build_end = "build_end"
    83     val isabelle_version = "isabelle_version"
    84     val afp_version = "afp_version"
    85   }
    86 
    87   object AFP
    88   {
    89     val Date_Format =
    90       Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    91         // workaround for jdk-8u102
    92         s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
    93     val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""")
    94     val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
    95     val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
    96     val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
    97     val settings =
    98       List("ISABELLE_BUILD_OPTIONS=", "ML_PLATFORM=", "ML_HOME=", "ML_SYSTEM=", "ML_OPTIONS=")
    99   }
   100 
   101   def parse_header(lines: List[String]): Header =
   102   {
   103     val proper_lines = lines.filterNot(line => line.forall(Character.isWhitespace(_)))
   104 
   105     def err(msg: String): Nothing = error(cat_lines((msg + ":") :: lines.take(10)))
   106 
   107     proper_lines match {
   108       case AFP.Test_Start(start, hostname) :: _ =>
   109         (start, proper_lines.last) match {
   110           case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
   111             val props =
   112               List(
   113                 Field.build_host -> hostname,
   114                 Field.build_start -> start_date.toString,
   115                 Field.build_end -> end_date.toString) :::
   116               lines.collectFirst(
   117                 { case AFP.Isabelle_Version(id) => Field.isabelle_version -> id }).toList :::
   118               lines.collectFirst(
   119                 { case AFP.AFP_Version(id) => Field.afp_version -> id }).toList
   120             val settings = lines.filter(line => AFP.settings.exists(line.startsWith(_)))
   121             Header(Header_Kind.AFP_TEST, props, settings)
   122           case _ => err("Malformed start/end date in afp-test log")
   123         }
   124       case _ => err("Failed to detect build log header")
   125     }
   126   }
   127 
   128   object Session_Status extends Enumeration
   129   {
   130     val UNKNOWN = Value("unknown")
   131     val FINISHED = Value("finished")
   132     val FAILED = Value("failed")
   133     val CANCELLED = Value("cancelled")
   134   }
   135 
   136 
   137   /* main log: produced by isatest, afp-test, jenkins etc. */
   138 
   139   sealed case class Info(
   140     ml_options: List[(String, String)],
   141     finished: Map[String, Timing],
   142     timing: Map[String, Timing],
   143     threads: Map[String, Int])
   144   {
   145     val sessions: Set[String] = finished.keySet ++ timing.keySet
   146 
   147     override def toString: String =
   148       sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")")
   149   }
   150 
   151   private val Session_Finished1 =
   152     new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   153   private val Session_Finished2 =
   154     new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   155   private val Session_Timing =
   156     new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   157 
   158   private object ML_Option
   159   {
   160     def unapply(s: String): Option[(String, String)] =
   161       s.indexOf('=') match {
   162         case -1 => None
   163         case i =>
   164           val a = s.substring(0, i)
   165           Library.try_unquote(s.substring(i + 1)) match {
   166             case Some(b) if Build.ml_options.contains(a) => Some((a, b))
   167             case _ => None
   168           }
   169       }
   170   }
   171 
   172   def parse_info(text: String): Info =
   173   {
   174     val ml_options = new mutable.ListBuffer[(String, String)]
   175     var finished = Map.empty[String, Timing]
   176     var timing = Map.empty[String, Timing]
   177     var threads = Map.empty[String, Int]
   178 
   179     for (line <- split_lines(text)) {
   180       line match {
   181         case Session_Finished1(name,
   182             Value.Int(e1), Value.Int(e2), Value.Int(e3),
   183             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   184           val elapsed = Time.hms(e1, e2, e3)
   185           val cpu = Time.hms(c1, c2, c3)
   186           finished += (name -> Timing(elapsed, cpu, Time.zero))
   187         case Session_Finished2(name,
   188             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   189           val elapsed = Time.hms(e1, e2, e3)
   190           finished += (name -> Timing(elapsed, Time.zero, Time.zero))
   191         case Session_Timing(name,
   192             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   193           val elapsed = Time.seconds(e)
   194           val cpu = Time.seconds(c)
   195           val gc = Time.seconds(g)
   196           timing += (name -> Timing(elapsed, cpu, gc))
   197           threads += (name -> t)
   198         case ML_Option(a, b) => ml_options += (a -> b)
   199         case _ =>
   200       }
   201     }
   202 
   203     Info(ml_options.toList, finished, timing, threads)
   204   }
   205 }