# HG changeset patch # User wenzelm # Date 1475745192 -7200 # Node ID a7352cbde7d724e710bc02f01679eb68199a5252 # Parent 1bbea2b55d2251de8eaa0b508c704ae283ba6f98 misc tuning and clarification; diff -r 1bbea2b55d22 -r a7352cbde7d7 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Oct 05 22:09:53 2016 +0200 +++ b/src/Pure/Tools/build.scala Thu Oct 06 11:13:12 2016 +0200 @@ -477,7 +477,7 @@ } try { - val info = Build_Log.parse_session_info(name, split_lines(text), false) + val info = Build_Log.Log_File(name, text).parse_session_info(name, false) val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0 (info.command_timings, session_timing) } diff -r 1bbea2b55d22 -r a7352cbde7d7 src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Wed Oct 05 22:09:53 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Thu Oct 06 11:13:12 2016 +0200 @@ -16,18 +16,73 @@ object Build_Log { - /* inlined properties (YXML) */ + /** log file **/ - object Props + object Log_File + { + def apply(name: String, lines: List[String]): Log_File = + new Log_File(name, lines) + + def apply(name: String, text: String): Log_File = + Log_File(name, split_lines(Library.trim_line(text)).map(Library.trim_line(_))) + } + + class Log_File private(val name: String, val lines: List[String]) { - def print(props: Properties.T): String = YXML.string_of_body(XML.Encode.properties(props)) - def parse(text: String): Properties.T = XML.Decode.properties(YXML.parse_body(text)) + log_file => + + override def toString: String = name + + def text: String = cat_lines(lines) + + def err(msg: String): Nothing = + error("Error in log file " + quote(name) + ": " + msg) + + + /* inlined content */ + + def find[A](f: String => Option[A]): Option[A] = + lines.iterator.map(f).find(_.isDefined).map(_.get) + + def find_match(regex: Regex): Option[String] = + lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1). + map(res => res.get.head) + + + /* settings */ + + def get_setting(setting: String): String = + lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting) - def parse_lines(prefix: String, lines: List[String]): List[Properties.T] = - for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s) + def get_settings(settings: List[String]): List[String] = + settings.map(get_setting(_)) + + + /* properties (YXML) */ + + val xml_cache = new XML.Cache() + + def parse_props(text: String): Properties.T = + xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) + + def filter_props(prefix: String): List[Properties.T] = + for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s) - def find_parse_line(prefix: String, lines: List[String]): Option[Properties.T] = - lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length))) + def find_line(prefix: String): Option[String] = + find(Library.try_unprefix(prefix, _)) + + def find_props(prefix: String): Option[Properties.T] = + find_line(prefix).map(parse_props(_)) + + + /* parse various formats */ + + def parse_session_info(session_name: String, full: Boolean): Session_Info = + Build_Log.parse_session_info(log_file, session_name, full) + + def parse_header: Header = Build_Log.parse_header(log_file) + + def parse_info: Info = Build_Log.parse_info(log_file) } @@ -40,31 +95,26 @@ ml_statistics: List[Properties.T], task_statistics: List[Properties.T]) - val SESSION_NAME = "\fSession.name = " - - def parse_session_info(name0: String, lines: List[String], full: Boolean): Session_Info = + private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info = { val xml_cache = new XML.Cache() - def parse_lines(prfx: String): List[Properties.T] = - Props.parse_lines(prfx, lines).map(xml_cache.props(_)) val session_name = - lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) match { + log_file.find_line("\fSession.name = ") match { case None => name0 case Some(name) if name0 == "" || name0 == name => name - case Some(name) => - error("Session log for " + quote(name0) + " is actually from " + quote(name)) + case Some(name) => log_file.err("log from different session " + quote(name)) } - val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil - val command_timings = parse_lines("\fcommand_timing = ") - val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil - val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil + val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil + val command_timings = log_file.filter_props("\fcommand_timing = ") + val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil + val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics) } - /* header and data fields */ + /* header and meta data */ object Header_Kind extends Enumeration { @@ -84,44 +134,47 @@ val afp_version = "afp_version" } + val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") + object AFP { val Date_Format = Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), // workaround for jdk-8u102 s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a }))) + val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""") val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""") val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""") val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""") - val settings = - List("ISABELLE_BUILD_OPTIONS=", "ML_PLATFORM=", "ML_HOME=", "ML_SYSTEM=", "ML_OPTIONS=") + val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings } - def parse_header(lines: List[String]): Header = + private def parse_header(log_file: Log_File): Header = { - val proper_lines = lines.filterNot(line => line.forall(Character.isWhitespace(_))) - - def err(msg: String): Nothing = error(cat_lines((msg + ":") :: lines.take(10))) + log_file.lines match { + case AFP.Test_Start(start, hostname) :: _ => + (start, log_file.lines.last) match { + case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) => + val isabelle_version = + log_file.find_match(AFP.Isabelle_Version) getOrElse + log_file.err("missing Isabelle version") + val afp_version = + log_file.find_match(AFP.AFP_Version) getOrElse + log_file.err("missing AFP version") - proper_lines match { - case AFP.Test_Start(start, hostname) :: _ => - (start, proper_lines.last) match { - case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) => - val props = + Header(Header_Kind.AFP_TEST, List( Field.build_host -> hostname, Field.build_start -> start_date.toString, - Field.build_end -> end_date.toString) ::: - lines.collectFirst( - { case AFP.Isabelle_Version(id) => Field.isabelle_version -> id }).toList ::: - lines.collectFirst( - { case AFP.AFP_Version(id) => Field.afp_version -> id }).toList - val settings = lines.filter(line => AFP.settings.exists(line.startsWith(_))) - Header(Header_Kind.AFP_TEST, props, settings) - case _ => err("Malformed start/end date in afp-test log") + Field.build_end -> end_date.toString, + Field.isabelle_version -> isabelle_version, + Field.afp_version -> afp_version), + log_file.get_settings(AFP.settings)) + + case _ => log_file.err("cannot detect start/end date in afp-test log") } - case _ => err("Failed to detect build log header") + case _ => log_file.err("cannot detect log header format") } } @@ -169,14 +222,14 @@ } } - def parse_info(text: String): Info = + private def parse_info(log_file: Log_File): Info = { val ml_options = new mutable.ListBuffer[(String, String)] var finished = Map.empty[String, Timing] var timing = Map.empty[String, Timing] var threads = Map.empty[String, Int] - for (line <- split_lines(text)) { + for (line <- log_file.lines) { line match { case Session_Finished1(name, Value.Int(e1), Value.Int(e2), Value.Int(e3), diff -r 1bbea2b55d22 -r a7352cbde7d7 src/Pure/Tools/build_stats.scala --- a/src/Pure/Tools/build_stats.scala Wed Oct 05 22:09:53 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Thu Oct 06 11:13:12 2016 +0200 @@ -29,7 +29,7 @@ val all_infos = Par_List.map((job_info: CI_API.Job_Info) => - (job_info.timestamp / 1000, Build_Log.parse_info(Url.read(job_info.output))), job_infos) + (job_info.timestamp / 1000, job_info.read_output.parse_info), job_infos) val all_sessions = (Set.empty[String] /: all_infos)( { case (s, (_, info)) => s ++ info.sessions }) diff -r 1bbea2b55d22 -r a7352cbde7d7 src/Pure/Tools/ci_api.scala --- a/src/Pure/Tools/ci_api.scala Wed Oct 05 22:09:53 2016 +0200 +++ b/src/Pure/Tools/ci_api.scala Thu Oct 06 11:13:12 2016 +0200 @@ -44,12 +44,12 @@ output: URL, session_logs: List[(String, URL)]) { - def read_output(): String = Url.read(output) + def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) def read_log(name: String, full: Boolean): Build_Log.Session_Info = { val text = session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "" - Build_Log.parse_session_info(name, split_lines(text), full) + Build_Log.Log_File(name, text).parse_session_info(name, full) } }