# HG changeset patch # User wenzelm # Date 1475853167 -7200 # Node ID 1c451e5c145f82f648a796a4f30df54687694e65 # Parent bca58a11efde1948b4d774c3976ee5a561504d9f clarified parse_build_info: isabelle build output; clarified Session_Status; tuned signature; diff -r bca58a11efde -r 1c451e5c145f src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Fri Oct 07 16:50:47 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Fri Oct 07 17:12:47 2016 +0200 @@ -119,16 +119,16 @@ /* parse various formats */ def parse_session_info( - session_name: String, + default_name: String = "", command_timings: Boolean = false, ml_statistics: Boolean = false, task_statistics: Boolean = false): Session_Info = Build_Log.parse_session_info( - log_file, session_name, command_timings, ml_statistics, task_statistics) + log_file, default_name, command_timings, ml_statistics, task_statistics) - def parse_header: Header = Build_Log.parse_header(log_file) + def parse_header(): Header = Build_Log.parse_header(log_file) - def parse_info: Info = Build_Log.parse_info(log_file) + def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file) } @@ -230,68 +230,128 @@ } } + + /* build info: produced by isabelle build */ + object Session_Status extends Enumeration { - val UNKNOWN = Value("unknown") + val EXISTING = Value("existing") val FINISHED = Value("finished") val FAILED = Value("failed") val CANCELLED = Value("cancelled") } - - /* main log: produced by isatest, afp-test, jenkins etc. */ + sealed case class Session_Entry( + chapter: String, + groups: List[String], + threads: Option[Int], + timing: Option[Timing], + ml_timing: Option[Timing], + status: Session_Status.Value) + { + def ok: Boolean = status == Session_Status.EXISTING || status == Session_Status.FINISHED + def finished: Boolean = status == Session_Status.FINISHED + } - sealed case class Info( - settings: List[(String, String)], - finished: Map[String, Timing], - timing: Map[String, Timing], - threads: Map[String, Int]) + sealed case class Build_Info(sessions: Map[String, Session_Entry]) { - val sessions: Set[String] = finished.keySet ++ timing.keySet + def session(name: String): Session_Entry = sessions(name) + def get_session(name: String): Option[Session_Entry] = sessions.get(name) - override def toString: String = - sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")") + def finished(name: String): Boolean = + get_session(name) match { + case Some(entry) => entry.finished + case None => false + } + + def timing(name: String): Timing = + (for (entry <- get_session(name); t <- entry.timing) yield t) getOrElse Timing.zero + + def ml_timing(name: String): Timing = + (for (entry <- get_session(name); t <- entry.ml_timing) yield t) getOrElse Timing.zero } - private val Session_Finished1 = - new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") - private val Session_Finished2 = - new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""") - private val Session_Timing = - new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") + private def parse_build_info(log_file: Log_File): Build_Info = + { + object Chapter_Name + { + def unapply(s: String): Some[(String, String)] = + space_explode('/', s) match { + case List(chapter, name) => Some((chapter, name)) + case _ => Some(("", s)) + } + } - private def parse_info(log_file: Log_File): Info = - { - val settings = new mutable.ListBuffer[(String, String)] - var finished = Map.empty[String, Timing] + val Session_No_Groups = new Regex("""^Session (\S+)$""") + val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""") + val Session_Finished1 = + new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") + val Session_Finished2 = + new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""") + val Session_Timing = + new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") + val Session_Failed = new Regex("""^(\S+) FAILED""") + val Session_Cancelled = new Regex("""^(\S+) CANCELLED""") + + var chapter = Map.empty[String, String] + var groups = Map.empty[String, List[String]] + var threads = Map.empty[String, Int] var timing = Map.empty[String, Timing] - var threads = Map.empty[String, Int] + var ml_timing = Map.empty[String, Timing] + var failed = Set.empty[String] + var cancelled = Set.empty[String] + def all_sessions: Set[String] = + chapter.keySet ++ groups.keySet ++ threads.keySet ++ + timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled + for (line <- log_file.lines) { line match { + case Session_No_Groups(Chapter_Name(chapt, name)) => + chapter += (name -> chapt) + groups += (name -> Nil) + case Session_Groups(Chapter_Name(chapt, name), grps) => + chapter += (name -> chapt) + groups += (name -> Word.explode(grps)) case Session_Finished1(name, Value.Int(e1), Value.Int(e2), Value.Int(e3), Value.Int(c1), Value.Int(c2), Value.Int(c3)) => val elapsed = Time.hms(e1, e2, e3) val cpu = Time.hms(c1, c2, c3) - finished += (name -> Timing(elapsed, cpu, Time.zero)) + timing += (name -> Timing(elapsed, cpu, Time.zero)) case Session_Finished2(name, Value.Int(e1), Value.Int(e2), Value.Int(e3)) => val elapsed = Time.hms(e1, e2, e3) - finished += (name -> Timing(elapsed, Time.zero, Time.zero)) + timing += (name -> Timing(elapsed, Time.zero, Time.zero)) case Session_Timing(name, Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) => val elapsed = Time.seconds(e) val cpu = Time.seconds(c) val gc = Time.seconds(g) - timing += (name -> Timing(elapsed, cpu, gc)) + ml_timing += (name -> Timing(elapsed, cpu, gc)) threads += (name -> t) - case Settings.Entry(a, b) if Settings.all_settings.contains(a) => - settings += (a -> b) case _ => } } - Info(settings.toList, finished, timing, threads) + val sessions = + Map( + (for (name <- all_sessions.toList) yield { + val status = + if (failed(name)) Session_Status.FAILED + else if (cancelled(name)) Session_Status.CANCELLED + else if (timing.isDefinedAt(name)) Session_Status.FINISHED + else Session_Status.EXISTING + val entry = + Session_Entry( + chapter.getOrElse(name, ""), + groups.getOrElse(name, Nil), + threads.get(name), + timing.get(name), + ml_timing.get(name), + status) + (name -> entry) + }):_*) + Build_Info(sessions) } } diff -r bca58a11efde -r 1c451e5c145f src/Pure/Tools/build_stats.scala --- a/src/Pure/Tools/build_stats.scala Fri Oct 07 16:50:47 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Fri Oct 07 17:12:47 2016 +0200 @@ -29,16 +29,14 @@ val all_infos = Par_List.map((job_info: CI_API.Job_Info) => - (job_info.timestamp / 1000, job_info.read_output.parse_info), job_infos) + (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos) val all_sessions = (Set.empty[String] /: all_infos)( - { case (s, (_, info)) => s ++ info.sessions }) + { case (s, (_, info)) => s ++ info.sessions.keySet }) - def check_threshold(info: Build_Log.Info, session: String): Boolean = - info.finished.get(session) match { - case Some(t) => t.elapsed >= elapsed_threshold - case None => false - } + def check_threshold(info: Build_Log.Build_Info, session: String): Boolean = + (for (entry <- info.get_session(session); t <- entry.timing) + yield t.elapsed >= elapsed_threshold) getOrElse false val sessions = for { @@ -51,12 +49,16 @@ Isabelle_System.with_tmp_file(session, "png") { data_file => Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file => val data = - for { (t, info) <- all_infos if info.finished.isDefinedAt(session) } + for { (t, info) <- all_infos if info.finished(session) } yield { - val finished = info.finished.getOrElse(session, Timing.zero) - val timing = info.timing.getOrElse(session, Timing.zero) - List(t.toString, finished.elapsed.minutes, finished.cpu.minutes, - timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ") + val timing1 = info.timing(session) + val timing2 = info.ml_timing(session) + List(t.toString, + timing1.elapsed.minutes, + timing1.cpu.minutes, + timing2.elapsed.minutes, + timing2.cpu.minutes, + timing2.gc.minutes).mkString(" ") } File.write(data_file, cat_lines(data))