misc tuning and clarification;
authorwenzelm
Thu Oct 06 11:13:12 2016 +0200 (2016-10-06)
changeset 64062a7352cbde7d7
parent 64061 1bbea2b55d22
child 64063 2c5039363ea3
misc tuning and clarification;
src/Pure/Tools/build.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/build_stats.scala
src/Pure/Tools/ci_api.scala
     1.1 --- a/src/Pure/Tools/build.scala	Wed Oct 05 22:09:53 2016 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Thu Oct 06 11:13:12 2016 +0200
     1.3 @@ -477,7 +477,7 @@
     1.4        }
     1.5  
     1.6        try {
     1.7 -        val info = Build_Log.parse_session_info(name, split_lines(text), false)
     1.8 +        val info = Build_Log.Log_File(name, text).parse_session_info(name, false)
     1.9          val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.10          (info.command_timings, session_timing)
    1.11        }
     2.1 --- a/src/Pure/Tools/build_log.scala	Wed Oct 05 22:09:53 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Thu Oct 06 11:13:12 2016 +0200
     2.3 @@ -16,18 +16,73 @@
     2.4  
     2.5  object Build_Log
     2.6  {
     2.7 -  /* inlined properties (YXML) */
     2.8 +  /** log file **/
     2.9  
    2.10 -  object Props
    2.11 +  object Log_File
    2.12 +  {
    2.13 +    def apply(name: String, lines: List[String]): Log_File =
    2.14 +      new Log_File(name, lines)
    2.15 +
    2.16 +    def apply(name: String, text: String): Log_File =
    2.17 +      Log_File(name, split_lines(Library.trim_line(text)).map(Library.trim_line(_)))
    2.18 +  }
    2.19 +
    2.20 +  class Log_File private(val name: String, val lines: List[String])
    2.21    {
    2.22 -    def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props))
    2.23 -    def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text))
    2.24 +    log_file =>
    2.25 +
    2.26 +    override def toString: String = name
    2.27 +
    2.28 +    def text: String = cat_lines(lines)
    2.29 +
    2.30 +    def err(msg: String): Nothing =
    2.31 +      error("Error in log file " + quote(name) + ": " + msg)
    2.32 +
    2.33 +
    2.34 +    /* inlined content */
    2.35 +
    2.36 +    def find[A](f: String => Option[A]): Option[A] =
    2.37 +      lines.iterator.map(f).find(_.isDefined).map(_.get)
    2.38 +
    2.39 +    def find_match(regex: Regex): Option[String] =
    2.40 +      lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
    2.41 +        map(res => res.get.head)
    2.42 +
    2.43 +
    2.44 +    /* settings */
    2.45 +
    2.46 +    def get_setting(setting: String): String =
    2.47 +      lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting)
    2.48  
    2.49 -    def parse_lines(prefix: String, lines: List[String]): List[Properties.T] =
    2.50 -      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s)
    2.51 +    def get_settings(settings: List[String]): List[String] =
    2.52 +      settings.map(get_setting(_))
    2.53 +
    2.54 +
    2.55 +    /* properties (YXML) */
    2.56 +
    2.57 +    val xml_cache = new XML.Cache()
    2.58 +
    2.59 +    def parse_props(text: String): Properties.T =
    2.60 +      xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
    2.61 +
    2.62 +    def filter_props(prefix: String): List[Properties.T] =
    2.63 +      for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s)
    2.64  
    2.65 -    def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] =
    2.66 -      lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length)))
    2.67 +    def find_line(prefix: String): Option[String] =
    2.68 +      find(Library.try_unprefix(prefix, _))
    2.69 +
    2.70 +    def find_props(prefix: String): Option[Properties.T] =
    2.71 +      find_line(prefix).map(parse_props(_))
    2.72 +
    2.73 +
    2.74 +    /* parse various formats */
    2.75 +
    2.76 +    def parse_session_info(session_name: String, full: Boolean): Session_Info =
    2.77 +      Build_Log.parse_session_info(log_file, session_name, full)
    2.78 +
    2.79 +    def parse_header: Header = Build_Log.parse_header(log_file)
    2.80 +
    2.81 +    def parse_info: Info = Build_Log.parse_info(log_file)
    2.82    }
    2.83  
    2.84  
    2.85 @@ -40,31 +95,26 @@
    2.86      ml_statistics: List[Properties.T],
    2.87      task_statistics: List[Properties.T])
    2.88  
    2.89 -  val SESSION_NAME = "\fSession.name = "
    2.90 -
    2.91 -  def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info =
    2.92 +  private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info =
    2.93    {
    2.94      val xml_cache = new XML.Cache()
    2.95 -    def parse_lines(prfx: String): List[Properties.T] =
    2.96 -      Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    2.97  
    2.98      val session_name =
    2.99 -      lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match {
   2.100 +      log_file.find_line("\fSession.name = ") match {
   2.101          case None => name0
   2.102          case Some(name) if name0 == "" || name0 == name => name
   2.103 -        case Some(name) =>
   2.104 -          error("Session log for " + quote(name0) + " is actually from " + quote(name))
   2.105 +        case Some(name) => log_file.err("log from different session " + quote(name))
   2.106        }
   2.107 -    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
   2.108 -    val command_timings = parse_lines("\fcommand_timing = ")
   2.109 -    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
   2.110 -    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
   2.111 +    val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   2.112 +    val command_timings = log_file.filter_props("\fcommand_timing = ")
   2.113 +    val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil
   2.114 +    val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil
   2.115  
   2.116      Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
   2.117    }
   2.118  
   2.119  
   2.120 -  /* header and data fields */
   2.121 +  /* header and meta data */
   2.122  
   2.123    object Header_Kind extends Enumeration
   2.124    {
   2.125 @@ -84,44 +134,47 @@
   2.126      val afp_version = "afp_version"
   2.127    }
   2.128  
   2.129 +  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
   2.130 +
   2.131    object AFP
   2.132    {
   2.133      val Date_Format =
   2.134        Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
   2.135          // workaround for jdk-8u102
   2.136          s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
   2.137 +
   2.138      val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""")
   2.139      val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
   2.140      val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
   2.141      val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
   2.142 -    val settings =
   2.143 -      List("ISABELLE_BUILD_OPTIONS=", "ML_PLATFORM=", "ML_HOME=", "ML_SYSTEM=", "ML_OPTIONS=")
   2.144 +    val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings
   2.145    }
   2.146  
   2.147 -  def parse_header(lines: List[String]): Header =
   2.148 +  private def parse_header(log_file: Log_File): Header =
   2.149    {
   2.150 -    val proper_lines = lines.filterNot(line => line.forall(Character.isWhitespace(_)))
   2.151 -
   2.152 -    def err(msg: String): Nothing = error(cat_lines((msg + ":") :: lines.take(10)))
   2.153 +    log_file.lines match {
   2.154 +      case AFP.Test_Start(start, hostname) :: _ =>
   2.155 +        (start, log_file.lines.last) match {
   2.156 +          case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
   2.157 +            val isabelle_version =
   2.158 +              log_file.find_match(AFP.Isabelle_Version) getOrElse
   2.159 +                log_file.err("missing Isabelle version")
   2.160 +            val afp_version =
   2.161 +              log_file.find_match(AFP.AFP_Version) getOrElse
   2.162 +                log_file.err("missing AFP version")
   2.163  
   2.164 -    proper_lines match {
   2.165 -      case AFP.Test_Start(start, hostname) :: _ =>
   2.166 -        (start, proper_lines.last) match {
   2.167 -          case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
   2.168 -            val props =
   2.169 +            Header(Header_Kind.AFP_TEST,
   2.170                List(
   2.171                  Field.build_host -> hostname,
   2.172                  Field.build_start -> start_date.toString,
   2.173 -                Field.build_end -> end_date.toString) :::
   2.174 -              lines.collectFirst(
   2.175 -                { case AFP.Isabelle_Version(id) => Field.isabelle_version -> id }).toList :::
   2.176 -              lines.collectFirst(
   2.177 -                { case AFP.AFP_Version(id) => Field.afp_version -> id }).toList
   2.178 -            val settings = lines.filter(line => AFP.settings.exists(line.startsWith(_)))
   2.179 -            Header(Header_Kind.AFP_TEST, props, settings)
   2.180 -          case _ => err("Malformed start/end date in afp-test log")
   2.181 +                Field.build_end -> end_date.toString,
   2.182 +                Field.isabelle_version -> isabelle_version,
   2.183 +                Field.afp_version -> afp_version),
   2.184 +              log_file.get_settings(AFP.settings))
   2.185 +
   2.186 +          case _ => log_file.err("cannot detect start/end date in afp-test log")
   2.187          }
   2.188 -      case _ => err("Failed to detect build log header")
   2.189 +      case _ => log_file.err("cannot detect log header format")
   2.190      }
   2.191    }
   2.192  
   2.193 @@ -169,14 +222,14 @@
   2.194        }
   2.195    }
   2.196  
   2.197 -  def parse_info(text: String): Info =
   2.198 +  private def parse_info(log_file: Log_File): Info =
   2.199    {
   2.200      val ml_options = new mutable.ListBuffer[(String, String)]
   2.201      var finished = Map.empty[String, Timing]
   2.202      var timing = Map.empty[String, Timing]
   2.203      var threads = Map.empty[String, Int]
   2.204  
   2.205 -    for (line <- split_lines(text)) {
   2.206 +    for (line <- log_file.lines) {
   2.207        line match {
   2.208          case Session_Finished1(name,
   2.209              Value.Int(e1), Value.Int(e2), Value.Int(e3),
     3.1 --- a/src/Pure/Tools/build_stats.scala	Wed Oct 05 22:09:53 2016 +0200
     3.2 +++ b/src/Pure/Tools/build_stats.scala	Thu Oct 06 11:13:12 2016 +0200
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5      val all_infos =
     3.6        Par_List.map((job_info: CI_API.Job_Info) =>
     3.7 -        (job_info.timestamp / 1000, Build_Log.parse_info(Url.read(job_info.output))), job_infos)
     3.8 +        (job_info.timestamp / 1000, job_info.read_output.parse_info), job_infos)
     3.9      val all_sessions =
    3.10        (Set.empty[String] /: all_infos)(
    3.11          { case (s, (_, info)) => s ++ info.sessions })
     4.1 --- a/src/Pure/Tools/ci_api.scala	Wed Oct 05 22:09:53 2016 +0200
     4.2 +++ b/src/Pure/Tools/ci_api.scala	Thu Oct 06 11:13:12 2016 +0200
     4.3 @@ -44,12 +44,12 @@
     4.4      output: URL,
     4.5      session_logs: List[(String, URL)])
     4.6    {
     4.7 -    def read_output(): String = Url.read(output)
     4.8 +    def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
     4.9      def read_log(name: String, full: Boolean): Build_Log.Session_Info =
    4.10      {
    4.11        val text =
    4.12          session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    4.13 -      Build_Log.parse_session_info(name, split_lines(text), full)
    4.14 +      Build_Log.Log_File(name, text).parse_session_info(name, full)
    4.15      }
    4.16    }
    4.17