--- 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)
+ }
}
--- 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</ul>\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(", ", ", ")")
-}
--- 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)
}
}
}