src/Pure/Tools/build_log.scala
changeset 64062 a7352cbde7d7
parent 64061 1bbea2b55d22
child 64063 2c5039363ea3
     1.1 --- a/src/Pure/Tools/build_log.scala	Wed Oct 05 22:09:53 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Thu Oct 06 11:13:12 2016 +0200
     1.3 @@ -16,18 +16,73 @@
     1.4  
     1.5  object Build_Log
     1.6  {
     1.7 -  /* inlined properties (YXML) */
     1.8 +  /** log file **/
     1.9  
    1.10 -  object Props
    1.11 +  object Log_File
    1.12 +  {
    1.13 +    def apply(name: String, lines: List[String]): Log_File =
    1.14 +      new Log_File(name, lines)
    1.15 +
    1.16 +    def apply(name: String, text: String): Log_File =
    1.17 +      Log_File(name, split_lines(Library.trim_line(text)).map(Library.trim_line(_)))
    1.18 +  }
    1.19 +
    1.20 +  class Log_File private(val name: String, val lines: List[String])
    1.21    {
    1.22 -    def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props))
    1.23 -    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    1.24 +    log_file =>
    1.25 +
    1.26 +    override def toString: String = name
    1.27 +
    1.28 +    def text: String = cat_lines(lines)
    1.29 +
    1.30 +    def err(msg: String): Nothing =
    1.31 +      error("Error in log file " + quote(name) + ": " + msg)
    1.32 +
    1.33 +
    1.34 +    /* inlined content */
    1.35 +
    1.36 +    def find[A](f: String => Option[A]): Option[A] =
    1.37 +      lines.iterator.map(f).find(_.isDefined).map(_.get)
    1.38 +
    1.39 +    def find_match(regex: Regex): Option[String] =
    1.40 +      lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
    1.41 +        map(res => res.get.head)
    1.42 +
    1.43 +
    1.44 +    /* settings */
    1.45 +
    1.46 +    def get_setting(setting: String): String =
    1.47 +      lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting)
    1.48  
    1.49 -    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    1.50 -      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    1.51 +    def get_settings(settings: List[String]): List[String] =
    1.52 +      settings.map(get_setting(_))
    1.53 +
    1.54 +
    1.55 +    /* properties (YXML) */
    1.56 +
    1.57 +    val xml_cache = new XML.Cache()
    1.58 +
    1.59 +    def parse_props(text: String): Properties.T =
    1.60 +      xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
    1.61 +
    1.62 +    def filter_props(prefix: String): List[Properties.T] =
    1.63 +      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s)
    1.64  
    1.65 -    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    1.66 -      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    1.67 +    def find_line(prefix: String): Option[String] =
    1.68 +      find(Library.try_unprefix(prefix, _))
    1.69 +
    1.70 +    def find_props(prefix: String): Option[Properties.T] =
    1.71 +      find_line(prefix).map(parse_props(_))
    1.72 +
    1.73 +
    1.74 +    /* parse various formats */
    1.75 +
    1.76 +    def parse_session_info(session_name: String, full: Boolean): Session_Info =
    1.77 +      Build_Log.parse_session_info(log_file, session_name, full)
    1.78 +
    1.79 +    def parse_header: Header = Build_Log.parse_header(log_file)
    1.80 +
    1.81 +    def parse_info: Info = Build_Log.parse_info(log_file)
    1.82    }
    1.83  
    1.84  
    1.85 @@ -40,31 +95,26 @@
    1.86      ml_statistics: List[Properties.T],
    1.87      task_statistics: List[Properties.T])
    1.88  
    1.89 -  val SESSION_NAME = "\fSession.name = "
    1.90 -
    1.91 -  def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    1.92 +  private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info =
    1.93    {
    1.94      val xml_cache = new XML.Cache()
    1.95 -    def parse_lines(prfx: String): List[Properties.T] =
    1.96 -      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    1.97  
    1.98      val session_name =
    1.99 -      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
   1.100 +      log_file.find_line("\fSession.name = ") match {
   1.101          case None => name0
   1.102          case Some(name) if name0 == "" || name0 == name => name
   1.103 -        case Some(name) =>
   1.104 -          error("Session log for " + quote(name0) + " is actually from " + quote(name))
   1.105 +        case Some(name) => log_file.err("log from different session " + quote(name))
   1.106        }
   1.107 -    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
   1.108 -    val command_timings = parse_lines("\fcommand_timing = ")
   1.109 -    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
   1.110 -    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
   1.111 +    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   1.112 +    val command_timings = log_file.filter_props("\fcommand_timing = ")
   1.113 +    val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil
   1.114 +    val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil
   1.115  
   1.116      Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
   1.117    }
   1.118  
   1.119  
   1.120 -  /* header and data fields */
   1.121 +  /* header and meta data */
   1.122  
   1.123    object Header_Kind extends Enumeration
   1.124    {
   1.125 @@ -84,44 +134,47 @@
   1.126      val afp_version = "afp_version"
   1.127    }
   1.128  
   1.129 +  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
   1.130 +
   1.131    object AFP
   1.132    {
   1.133      val Date_Format =
   1.134        Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
   1.135          // workaround for jdk-8u102
   1.136          s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
   1.137 +
   1.138      val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""")
   1.139      val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
   1.140      val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
   1.141      val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
   1.142 -    val settings =
   1.143 -      List("ISABELLE_BUILD_OPTIONS=", "ML_PLATFORM=", "ML_HOME=", "ML_SYSTEM=", "ML_OPTIONS=")
   1.144 +    val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings
   1.145    }
   1.146  
   1.147 -  def parse_header(lines: List[String]): Header =
   1.148 +  private def parse_header(log_file: Log_File): Header =
   1.149    {
   1.150 -    val proper_lines = lines.filterNot(line => line.forall(Character.isWhitespace(_)))
   1.151 -
   1.152 -    def err(msg: String): Nothing = error(cat_lines((msg + ":") :: lines.take(10)))
   1.153 +    log_file.lines match {
   1.154 +      case AFP.Test_Start(start, hostname) :: _ =>
   1.155 +        (start, log_file.lines.last) match {
   1.156 +          case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
   1.157 +            val isabelle_version =
   1.158 +              log_file.find_match(AFP.Isabelle_Version) getOrElse
   1.159 +                log_file.err("missing Isabelle version")
   1.160 +            val afp_version =
   1.161 +              log_file.find_match(AFP.AFP_Version) getOrElse
   1.162 +                log_file.err("missing AFP version")
   1.163  
   1.164 -    proper_lines match {
   1.165 -      case AFP.Test_Start(start, hostname) :: _ =>
   1.166 -        (start, proper_lines.last) match {
   1.167 -          case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
   1.168 -            val props =
   1.169 +            Header(Header_Kind.AFP_TEST,
   1.170                List(
   1.171                  Field.build_host -> hostname,
   1.172                  Field.build_start -> start_date.toString,
   1.173 -                Field.build_end -> end_date.toString) :::
   1.174 -              lines.collectFirst(
   1.175 -                { case AFP.Isabelle_Version(id) => Field.isabelle_version -> id }).toList :::
   1.176 -              lines.collectFirst(
   1.177 -                { case AFP.AFP_Version(id) => Field.afp_version -> id }).toList
   1.178 -            val settings = lines.filter(line => AFP.settings.exists(line.startsWith(_)))
   1.179 -            Header(Header_Kind.AFP_TEST, props, settings)
   1.180 -          case _ => err("Malformed start/end date in afp-test log")
   1.181 +                Field.build_end -> end_date.toString,
   1.182 +                Field.isabelle_version -> isabelle_version,
   1.183 +                Field.afp_version -> afp_version),
   1.184 +              log_file.get_settings(AFP.settings))
   1.185 +
   1.186 +          case _ => log_file.err("cannot detect start/end date in afp-test log")
   1.187          }
   1.188 -      case _ => err("Failed to detect build log header")
   1.189 +      case _ => log_file.err("cannot detect log header format")
   1.190      }
   1.191    }
   1.192  
   1.193 @@ -169,14 +222,14 @@
   1.194        }
   1.195    }
   1.196  
   1.197 -  def parse_info(text: String): Info =
   1.198 +  private def parse_info(log_file: Log_File): Info =
   1.199    {
   1.200      val ml_options = new mutable.ListBuffer[(String, String)]
   1.201      var finished = Map.empty[String, Timing]
   1.202      var timing = Map.empty[String, Timing]
   1.203      var threads = Map.empty[String, Int]
   1.204  
   1.205 -    for (line <- split_lines(text)) {
   1.206 +    for (line <- log_file.lines) {
   1.207        line match {
   1.208          case Session_Finished1(name,
   1.209              Value.Int(e1), Value.Int(e2), Value.Int(e3),