# HG changeset patch # User wenzelm # Date 1475669754 -7200 # Node ID 1fc9ab31720d1f06d56c0a956a38d34f015799d8 # Parent 7ece2e14fd6c16f31722582a67d627caa49f9f3d clarified modules; diff -r 7ece2e14fd6c -r 1fc9ab31720d src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Wed Oct 05 13:56:19 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Wed Oct 05 14:15:54 2016 +0200 @@ -7,6 +7,10 @@ package isabelle +import scala.collection.mutable +import scala.util.matching.Regex + + object Build_Log { /* inlined properties (YXML) */ @@ -55,4 +59,74 @@ Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics) } + + + /* main log: produced by isatest, afp-test, jenkins etc. */ + + sealed case class Info( + ml_options: List[(String, String)], + finished: Map[String, Timing], + timing: Map[String, Timing], + threads: Map[String, Int]) + { + val sessions: Set[String] = finished.keySet ++ timing.keySet + + override def toString: String = + sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")") + } + + 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 object ML_Option + { + def unapply(s: String): Option[(String, String)] = + s.indexOf('=') match { + case -1 => None + case i => + val a = s.substring(0, i) + Library.try_unquote(s.substring(i + 1)) match { + case Some(b) if Build.ml_options.contains(a) => Some((a, b)) + case _ => None + } + } + } + + def parse_info(text: String): 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)) { + line match { + 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)) + 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)) + 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)) + threads += (name -> t) + case ML_Option(a, b) => ml_options += (a -> b) + case _ => + } + } + + Info(ml_options.toList, finished, timing, threads) + } } diff -r 7ece2e14fd6c -r 1fc9ab31720d src/Pure/Tools/build_stats.scala --- a/src/Pure/Tools/build_stats.scala Wed Oct 05 13:56:19 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Wed Oct 05 14:15:54 2016 +0200 @@ -7,70 +7,8 @@ package isabelle -import scala.collection.mutable -import scala.util.matching.Regex - - object Build_Stats { - /* parse build output */ - - 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 object ML_Option - { - def unapply(s: String): Option[(String, String)] = - s.indexOf('=') match { - case -1 => None - case i => - val a = s.substring(0, i) - Library.try_unquote(s.substring(i + 1)) match { - case Some(b) if Build.ml_options.contains(a) => Some((a, b)) - case _ => None - } - } - } - - def parse(text: String): Build_Stats = - { - 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)) { - line match { - 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)) - 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)) - 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)) - threads += (name -> t) - case ML_Option(a, b) => ml_options += (a -> b) - case _ => - } - } - - Build_Stats(ml_options.toList, finished, timing, threads) - } - - /* presentation */ private val default_history_length = 100 @@ -86,18 +24,18 @@ elapsed_threshold: Time = default_elapsed_threshold, ml_timing: Option[Boolean] = default_ml_timing): List[String] = { - val build_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length) - if (build_infos.isEmpty) error("No build infos for job " + quote(job)) + val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length) + if (job_infos.isEmpty) error("No build infos for job " + quote(job)) - val all_build_stats = - Par_List.map((info: CI_API.Build_Info) => - (info.timestamp / 1000, parse(Url.read(info.output))), build_infos) + 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) val all_sessions = - (Set.empty[String] /: all_build_stats)( - { case (s, (_, stats)) => s ++ stats.sessions }) + (Set.empty[String] /: all_infos)( + { case (s, (_, info)) => s ++ info.sessions }) - def check_threshold(stats: Build_Stats, session: String): Boolean = - stats.finished.get(session) match { + 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 } @@ -105,7 +43,7 @@ val sessions = for { session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions) - if all_build_stats.filter({ case (_, stats) => check_threshold(stats, session) }).length >= 3 + if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3 } yield session Isabelle_System.mkdirs(dir) @@ -113,10 +51,10 @@ Isabelle_System.with_tmp_file(session, "png") { data_file => Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file => val data = - for { (t, stats) <- all_build_stats if stats.finished.isDefinedAt(session) } + for { (t, info) <- all_infos if info.finished.isDefinedAt(session) } yield { - val finished = stats.finished.getOrElse(session, Timing.zero) - val timing = stats.timing.getOrElse(session, Timing.zero) + 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(" ") } @@ -247,15 +185,3 @@ "\n\n" + html_footer) }) } - -sealed case class Build_Stats( - ml_options: List[(String, String)], - finished: Map[String, Timing], - timing: Map[String, Timing], - threads: Map[String, Int]) -{ - val sessions: Set[String] = finished.keySet ++ timing.keySet - - override def toString: String = - sessions.toList.sorted.mkString("Build_Stats(", ", ", ")") -} diff -r 7ece2e14fd6c -r 1fc9ab31720d src/Pure/Tools/ci_api.scala --- a/src/Pure/Tools/ci_api.scala Wed Oct 05 13:56:19 2016 +0200 +++ b/src/Pure/Tools/ci_api.scala Wed Oct 05 14:15:54 2016 +0200 @@ -38,7 +38,7 @@ name <- JSON.string(job, "name") } yield name - sealed case class Build_Info( + sealed case class Job_Info( job_name: String, timestamp: Long, output: URL, @@ -53,7 +53,7 @@ } } - def build_job_builds(job_name: String): List[Build_Info] = + def build_job_builds(job_name: String): List[Job_Info] = { val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""") @@ -71,7 +71,7 @@ log_path <- JSON.string(artifact, "relativePath") session <- (log_path match { case Log_Session(name) => Some(name) case _ => None }) } yield (session -> Url(job_prefix + "/artifact/" + log_path)) - Build_Info(job_name, timestamp, output, session_logs) + Job_Info(job_name, timestamp, output, session_logs) } } }