# HG changeset patch # User wenzelm # Date 1475940619 -7200 # Node ID 84c1ae86b9af4e16ee9b235fe2d672ed1e28190d # Parent 331fbf2a0d2ddf892f7623f5949950a9f4c8c83e# Parent b2290b9d017519a1aedae139454f2717c2149067 merged diff -r 331fbf2a0d2d -r 84c1ae86b9af src/Pure/General/date.scala --- a/src/Pure/General/date.scala Sat Oct 08 13:50:25 2016 +0200 +++ b/src/Pure/General/date.scala Sat Oct 08 17:30:19 2016 +0200 @@ -21,58 +21,54 @@ object Format { - def make(fmts: List[DateTimeFormatter], filter: String => String = s => s): Format = + def make(fmts: List[DateTimeFormatter], tune: String => String = s => s): Format = { require(fmts.nonEmpty) - @tailrec def parse_first( - last_exn: Option[Throwable], fs: List[DateTimeFormatter], str: String): TemporalAccessor = - { - fs match { - case Nil => throw last_exn.get - case f :: rest => - try { ZonedDateTime.from(f.parse(str)) } - catch { case exn: DateTimeParseException => parse_first(Some(exn), rest, str) } - } - } new Format { def apply(date: Date): String = fmts.head.format(date.rep) def parse(str: String): Date = - new Date(ZonedDateTime.from(parse_first(None, fmts, filter(str)))) + new Date(ZonedDateTime.from(Formatter.try_variants(fmts, tune(str)))) } } - def make_variants(patterns: List[String], - locales: List[Locale] = List(Locale.ROOT), - filter: String => String = s => s): Format = - { - val fmts = - patterns.flatMap(pat => - { - val fmt = DateTimeFormatter.ofPattern(pat) - locales.map(fmt.withLocale(_)) - }) - make(fmts, filter) - } + def apply(pats: String*): Format = + make(pats.toList.map(Date.Formatter.pattern(_))) - def apply(patterns: String*): Format = - make(patterns.toList.map(DateTimeFormatter.ofPattern(_))) - - val default: Format = apply("dd-MMM-uuuu HH:mm:ss xx") - val date: Format = apply("dd-MMM-uuuu") - val time: Format = apply("HH:mm:ss") + val default: Format = Format("dd-MMM-uuuu HH:mm:ss xx") + val date: Format = Format("dd-MMM-uuuu") + val time: Format = Format("HH:mm:ss") } abstract class Format private { def apply(date: Date): String def parse(str: String): Date + def unapply(str: String): Option[Date] = - try { Some(parse(str)) } - catch { case _: DateTimeParseException => None } - object Strict + try { Some(parse(str)) } catch { case _: DateTimeParseException => None } + } + + object Formatter + { + def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat) + + def variants(pats: List[String], locs: List[Locale] = Nil): List[DateTimeFormatter] = + pats.flatMap(pat => { + val fmt = pattern(pat) + if (locs.isEmpty) List(fmt) else locs.map(fmt.withLocale(_)) + }) + + @tailrec def try_variants(fmts: List[DateTimeFormatter], str: String, + last_exn: Option[DateTimeParseException] = None): TemporalAccessor = { - def unapply(s: String): Some[Date] = Some(parse(s)) + fmts match { + case Nil => + throw last_exn.getOrElse(new DateTimeParseException("Failed to parse date", str, 0)) + case fmt :: rest => + try { ZonedDateTime.from(fmt.parse(str)) } + catch { case exn: DateTimeParseException => try_variants(rest, str, Some(exn)) } + } } } @@ -89,6 +85,9 @@ sealed case class Date(rep: ZonedDateTime) { + def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone)) + def to_utc: Date = to(ZoneId.of("UTC")) + def time: Time = Time.instant(Instant.from(rep)) def timezone: ZoneId = rep.getZone diff -r 331fbf2a0d2d -r 84c1ae86b9af src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Sat Oct 08 13:50:25 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Sat Oct 08 17:30:19 2016 +0200 @@ -1,16 +1,16 @@ /* Title: Pure/Tools/build_log.scala Author: Makarius -Build log parsing for historic versions, back to "build_history_base". +Build log parsing for current and historic formats. */ package isabelle +import java.io.{File => JFile} +import java.time.ZoneId +import java.time.format.{DateTimeFormatter, DateTimeParseException} import java.util.Locale -import java.io.{File => JFile} -import java.time.ZonedDateTime -import java.time.format.{DateTimeFormatter, DateTimeParseException} import scala.collection.mutable import scala.util.matching.Regex @@ -18,6 +18,19 @@ object Build_Log { + /** directory content **/ + + def is_log(file: JFile): Boolean = + List(".log", ".log.gz", ".log.xz").exists(ext => file.getName.endsWith(ext)) + + def isatest_files(dir: Path): List[JFile] = + File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("isatest-makeall-")) + + def afp_test_files(dir: Path): List[JFile] = + File.find_files(dir.file, file => is_log(file) && file.getName.startsWith("afp-test-devel-")) + + + /** settings **/ object Settings @@ -49,6 +62,7 @@ } + /** log file **/ object Log_File @@ -75,6 +89,49 @@ } def apply(path: Path): Log_File = apply(path.file) + + + /* date format */ + + val Date_Format = + { + val fmts = + Date.Formatter.variants( + List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), + List(Locale.ENGLISH, Locale.GERMAN)) ::: + List( + DateTimeFormatter.RFC_1123_DATE_TIME, + Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin"))) + + def tune_timezone(s: String): String = + s match { + case "CET" | "MET" => "GMT+1" + case "CEST" | "MEST" => "GMT+2" + case "EST" => "Europe/Berlin" + case _ => s + } + def tune_weekday(s: String): String = + s match { + case "Die" => "Di" + case "Mit" => "Mi" + case "Don" => "Do" + case "Fre" => "Fr" + case "Sam" => "Sa" + case "Son" => "So" + case _ => s + } + + def tune(s: String): String = + Word.implode( + Word.explode(s) match { + case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_)) + case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_)) + case Nil => Nil + } + ) + + Date.Format.make(fmts, tune) + } } class Log_File private(val name: String, val lines: List[String]) @@ -89,6 +146,16 @@ error("Error in log file " + quote(name) + ": " + msg) + /* date format */ + + object Strict_Date + { + def unapply(s: String): Some[Date] = + try { Some(Log_File.Date_Format.parse(s)) } + catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) } + } + + /* inlined content */ def find[A](f: String => Option[A]): Option[A] = @@ -130,6 +197,10 @@ /* parse various formats */ + def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file) + + def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file) + def parse_session_info( default_name: String = "", command_timings: Boolean = false, @@ -137,74 +208,15 @@ task_statistics: Boolean = false): Session_Info = Build_Log.parse_session_info( log_file, default_name, command_timings, ml_statistics, task_statistics) - - def parse_header(): Header = Build_Log.parse_header(log_file) - - def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file) } - /* session log: produced by "isabelle build" */ - sealed case class Session_Info( - session_name: String, - session_timing: Properties.T, - command_timings: List[Properties.T], - ml_statistics: List[Properties.T], - task_statistics: List[Properties.T]) - - private def parse_session_info( - log_file: Log_File, - default_name: String, - command_timings: Boolean, - ml_statistics: Boolean, - task_statistics: Boolean): Session_Info = - { - val xml_cache = new XML.Cache() - - val session_name = - log_file.find_line("\fSession.name = ") match { - case None => default_name - case Some(name) if default_name == "" || default_name == name => name - case Some(name) => log_file.err("log from different session " + quote(name)) - } - val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil - val command_timings_ = - if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil - val ml_statistics_ = - if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil - val task_statistics_ = - if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil - - Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_) - } - - - /* header and meta data */ - - val Date_Format = - Date.Format.make_variants( - List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), - List(Locale.ENGLISH, Locale.GERMAN), - // workaround for jdk-8u102 - s => Word.implode(Word.explode(s).map({ - case "CET" | "MET" => "GMT+1" - case "CEST" | "MEST" => "GMT+2" - case "EST" => "GMT+1" // FIXME ?? - case a => a }))) - - object Header_Kind extends Enumeration - { - val ISATEST = Value("isatest") - val AFP_TEST = Value("afp-test") - val JENKINS = Value("jenkins") - } - - sealed case class Header( - kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)]) + /** meta info **/ object Field { + val build_engine = "build_engine" val build_host = "build_host" val build_start = "build_start" val build_end = "build_end" @@ -212,66 +224,110 @@ val afp_version = "afp_version" } + object Meta_Info + { + val empty: Meta_Info = Meta_Info(Nil, Nil) + } + + sealed case class Meta_Info(props: Properties.T, settings: List[(String, String)]) + { + def is_empty: Boolean = props.isEmpty && settings.isEmpty + } + object Isatest { - val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""") - val Test_End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""") + val engine = "isatest" + val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""") + val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""") val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""") val No_AFP_Version = new Regex("""$.""") } - object AFP + object AFP_Test { - val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""") - val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""") - val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""") + val engine = "afp-test" + val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""") + val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""") + val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""") val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""") val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""") + val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""") } - private def parse_header(log_file: Log_File): Header = + object Jenkins { - def parse(kind: Header_Kind.Value, start: Date, hostname: String, - Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header = + val engine = "jenkins" + val Start = new Regex("""^Started .*$""") + val Start_Date = new Regex("""^Build started at (.+)$""") + val No_End = new Regex("""$.""") + val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""") + val AFP_Version = new Regex("""^AFP id (\S+)$""") + val CONFIGURATION = "=== CONFIGURATION ===" + val BUILD = "=== BUILD ===" + val FINISHED = "Finished: " + } + + private def parse_meta_info(log_file: Log_File): Meta_Info = + { + def parse(engine: String, host: String, start: Date, + End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info = { - val start_date = Field.build_start -> start.toString + val build_engine = if (engine == "") Nil else List(Field.build_engine -> engine) + val build_host = if (host == "") Nil else List(Field.build_host -> host) + + val start_date = List(Field.build_start -> start.toString) val end_date = log_file.lines.last match { - case Test_End(Date_Format.Strict(end_date)) => + case End(log_file.Strict_Date(end_date)) => List(Field.build_end -> end_date.toString) case _ => Nil } - val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname) - val isabelle_version = log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _) - val afp_version = log_file.find_match(AFP_Version).map(Field.afp_version -> _) - Header(kind, - start_date :: end_date ::: build_host ::: - isabelle_version.toList ::: afp_version.toList, + Meta_Info(build_engine ::: build_host ::: + start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList, log_file.get_settings(Settings.all_settings)) } log_file.lines match { - case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ => - parse(Header_Kind.ISATEST, start, hostname, - Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version) - case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ => - parse(Header_Kind.AFP_TEST, start, hostname, - AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version) - case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ => - parse(Header_Kind.AFP_TEST, start, "", - AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version) - case _ => log_file.err("cannot detect log header format") + case Isatest.Start(log_file.Strict_Date(start), host) :: _ => + parse(Isatest.engine, host, start, Isatest.End, + Isatest.Isabelle_Version, Isatest.No_AFP_Version) + + case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ => + parse(AFP_Test.engine, host, start, AFP_Test.End, + AFP_Test.Isabelle_Version, AFP_Test.AFP_Version) + + case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ => + parse(AFP_Test.engine, "", start, AFP_Test.End, + AFP_Test.Isabelle_Version, AFP_Test.AFP_Version) + + case Jenkins.Start() :: _ + if log_file.lines.contains(Jenkins.CONFIGURATION) || + log_file.lines.last.startsWith(Jenkins.FINISHED) => + log_file.lines.dropWhile(_ != Jenkins.BUILD) match { + case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ => + parse(Jenkins.engine, "", start.to(ZoneId.of("Europe/Berlin")), Jenkins.No_End, + Jenkins.Isabelle_Version, Jenkins.AFP_Version) + case _ => Meta_Info.empty + } + + case line :: _ if line.startsWith("\0") => Meta_Info.empty + case List(Isatest.End(_)) => Meta_Info.empty + case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty + case Nil => Meta_Info.empty + + case _ => log_file.err("cannot detect log file format") } } - /* build info: produced by isabelle build */ + + /** build info: produced by isabelle build **/ object Session_Status extends Enumeration { @@ -397,4 +453,41 @@ }):_*) Build_Info(sessions) } + + + + /** session info: produced by "isabelle build" **/ + + sealed case class Session_Info( + session_name: String, + session_timing: Properties.T, + command_timings: List[Properties.T], + ml_statistics: List[Properties.T], + task_statistics: List[Properties.T]) + + private def parse_session_info( + log_file: Log_File, + default_name: String, + command_timings: Boolean, + ml_statistics: Boolean, + task_statistics: Boolean): Session_Info = + { + val xml_cache = new XML.Cache() + + val session_name = + log_file.find_line("\fSession.name = ") match { + case None => default_name + case Some(name) if default_name == "" || default_name == name => name + case Some(name) => log_file.err("log from different session " + quote(name)) + } + val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil + val command_timings_ = + if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil + val ml_statistics_ = + if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil + val task_statistics_ = + if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil + + Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_) + } } diff -r 331fbf2a0d2d -r 84c1ae86b9af src/Pure/Tools/build_stats.scala --- a/src/Pure/Tools/build_stats.scala Sat Oct 08 13:50:25 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Sat Oct 08 17:30:19 2016 +0200 @@ -29,7 +29,7 @@ val all_infos = Par_List.map((job_info: CI_API.Job_Info) => - (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos) + (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos) val all_sessions = (Set.empty[String] /: all_infos)( { case (s, (_, info)) => s ++ info.sessions.keySet }) diff -r 331fbf2a0d2d -r 84c1ae86b9af src/Pure/Tools/ci_api.scala --- a/src/Pure/Tools/ci_api.scala Sat Oct 08 13:50:25 2016 +0200 +++ b/src/Pure/Tools/ci_api.scala Sat Oct 08 17:30:19 2016 +0200 @@ -44,8 +44,8 @@ output: URL, session_logs: List[(String, URL)]) { - def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) - def read_log_file(name: String): Build_Log.Log_File = + def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) + def read_session_log(name: String): Build_Log.Log_File = Build_Log.Log_File(name, session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "") }