--- a/src/Pure/Admin/build_stats.scala Sat May 06 12:59:16 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,278 +0,0 @@
-/* Title: Pure/Admin/build_stats.scala
- Author: Makarius
-
-Performance statistics from build log database.
-*/
-
-package isabelle
-
-
-object Build_Stats
-{
- private val default_target_dir = Path.explode("stats")
- private val default_history_length = 30
- private val default_image_size = (800, 600)
-
-
- /* data profiles */
-
- sealed case class Profile(name: String, sql: String)
- {
- def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
- {
- val sql_sessions =
- if (only_sessions.isEmpty) ""
- else
- only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
- .mkString("(", " OR ", ") AND ")
-
- Build_Log.Data.universal_table.select(columns, distinct = true,
- sql = "WHERE " +
- Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
- Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
- " AND " + sql_sessions + SQL.enclose(sql) +
- " ORDER BY " + Build_Log.Data.pull_date + " DESC")
- }
- }
-
- val standard_profiles: List[Profile] =
- Jenkins.build_log_profiles :::
- Isabelle_Cronjob.remote_builds.flatten.toList.map(r => Profile(r.name, r.sql))
-
- sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
- {
- def check(elapsed_threshold: Time): Boolean =
- !timing.is_zero && timing.elapsed >= elapsed_threshold
- }
-
- type Data = Map[String, Map[String, List[Entry]]]
-
-
- /* read data */
-
- def read_data(options: Options,
- profiles: List[Profile] = standard_profiles,
- progress: Progress = No_Progress,
- history_length: Int = default_history_length,
- only_sessions: Set[String] = Set.empty,
- elapsed_threshold: Time = Time.zero): Data =
- {
- var data: Data = Map.empty
-
- val store = Build_Log.store(options)
- using(store.open_database())(db =>
- {
- for (profile <- profiles) {
- progress.echo("input " + quote(profile.name))
- val columns =
- List(
- Build_Log.Data.pull_date,
- Build_Log.Settings.ML_PLATFORM,
- Build_Log.Data.session_name,
- Build_Log.Data.threads,
- Build_Log.Data.timing_elapsed,
- Build_Log.Data.timing_cpu,
- Build_Log.Data.timing_gc,
- Build_Log.Data.ml_timing_elapsed,
- Build_Log.Data.ml_timing_cpu,
- Build_Log.Data.ml_timing_gc)
-
- db.using_statement(profile.select(columns, history_length, only_sessions))(stmt =>
- {
- val res = stmt.execute_query()
- while (res.next()) {
- val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
- val threads = res.get_int(Build_Log.Data.threads)
- val name =
- profile.name +
- "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
- "_M" + threads.getOrElse(1)
-
- val session = res.string(Build_Log.Data.session_name)
- val entry =
- Entry(res.date(Build_Log.Data.pull_date),
- res.timing(
- Build_Log.Data.timing_elapsed,
- Build_Log.Data.timing_cpu,
- Build_Log.Data.timing_gc),
- res.timing(
- Build_Log.Data.ml_timing_elapsed,
- Build_Log.Data.ml_timing_cpu,
- Build_Log.Data.ml_timing_gc))
-
- val session_entries = data.getOrElse(name, Map.empty)
- val entries = session_entries.getOrElse(session, Nil)
- data += (name -> (session_entries + (session -> (entry :: entries))))
- }
- })
- }
- })
-
- for {
- (name, session_entries) <- data
- session_entries1 <-
- {
- val session_entries1 =
- for {
- (session, entries) <- session_entries
- if entries.filter(_.check(elapsed_threshold)).length >= 3
- } yield (session, entries)
- if (session_entries1.isEmpty) None
- else Some(session_entries1)
- }
- } yield (name, session_entries1)
- }
-
-
- /* present data */
-
- private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
-<head><title>Performance statistics from build log database</title></head>
-<body>
-"""
- private val html_footer = """
-</body>
-</html>
-"""
-
- def present_data(data: Data,
- progress: Progress = No_Progress,
- target_dir: Path = default_target_dir,
- image_size: (Int, Int) = default_image_size,
- ml_timing: Option[Boolean] = None)
- {
- val data_entries = data.toList.sortBy(_._1)
- for ((name, session_entries) <- data_entries) {
- val dir = target_dir + Path.explode(name)
- progress.echo("output " + dir)
- Isabelle_System.mkdirs(dir)
-
- for ((session, entries) <- session_entries) {
- Isabelle_System.with_tmp_file(session, "data") { data_file =>
- Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
-
- File.write(data_file,
- cat_lines(
- entries.map(entry =>
- List(entry.date.unix_epoch.toString,
- entry.timing.elapsed.minutes,
- entry.timing.cpu.minutes,
- entry.ml_timing.elapsed.minutes,
- entry.ml_timing.cpu.minutes,
- entry.ml_timing.gc.minutes).mkString(" "))))
-
- val plots1 =
- List(
- """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
- """ using 1:3 smooth csplines title "cpu time" """,
- """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
- """ using 1:2 smooth csplines title "elapsed time" """)
- val plots2 =
- List(
- """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
- """ using 1:5 smooth csplines title "ML cpu time" """,
- """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
- """ using 1:4 smooth csplines title "ML elapsed time" """,
- """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
- """ using 1:6 smooth csplines title "ML gc time" """)
- val plots =
- ml_timing match {
- case None => plots1
- case Some(false) => plots1 ::: plots2
- case Some(true) => plots2
- }
-
- File.write(gnuplot_file, """
-set terminal png size """ + image_size._1 + "," + image_size._2 + """
-set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
-set xdata time
-set timefmt "%s"
-set format x "%d-%b"
-set xlabel """ + quote(session) + """ noenhanced
-set key left top
-plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
-
- val result =
- Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
- if (result.rc != 0)
- result.error("Gnuplot failed for " + name + "/" + session).check
- }
- }
- }
-
- File.write(dir + Path.basic("index.html"),
- html_header + "\n<h1>" + HTML.output(name) + "</h1>\n" +
- cat_lines(
- session_entries.toList.map(_._1).sorted.map(session =>
- """<br/><img src=""" + quote(HTML.output(session + ".png")) + """><br/>""")) +
- "\n" + html_footer)
- }
-
- File.write(target_dir + Path.basic("index.html"),
- html_header + "\n<ul>\n" +
- cat_lines(
- data_entries.map(_._1).map(name =>
- """<li> <a href=""" + quote(HTML.output(name + "/index.html")) + """>""" +
- HTML.output(name) + """</a> </li>""")) +
- "\n</ul>\n" + html_footer)
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("build_stats", "present statistics from build log database", args =>
- {
- var target_dir = default_target_dir
- var ml_timing: Option[Boolean] = None
- var only_sessions = Set.empty[String]
- var elapsed_threshold = Time.zero
- var history_length = default_history_length
- var options = Options.init()
- var image_size = default_image_size
-
- val getopts = Getopts("""
-Usage: isabelle build_stats [OPTIONS]
-
- Options are:
- -D DIR target directory (default """ + default_target_dir + """)
- -M only ML timing
- -S SESSIONS only given SESSIONS (comma separated)
- -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
- -l LENGTH length of history (default """ + default_history_length + """)
- -m include ML timing
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
-
- Present performance statistics from build log database, which is specified
- via system options build_log_database_host, build_log_database_user etc.
-""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "M" -> (_ => ml_timing = Some(true)),
- "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
- "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
- "l:" -> (arg => history_length = Value.Int.parse(arg)),
- "m" -> (_ => ml_timing = Some(false)),
- "o:" -> (arg => options = options + arg),
- "s:" -> (arg =>
- space_explode('x', arg).map(Value.Int.parse(_)) match {
- case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
- case _ => error("Error bad PNG image size: " + quote(arg))
- }))
-
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
-
- val progress = new Console_Progress
-
- val data =
- read_data(options, profiles = standard_profiles, progress = progress,
- history_length = history_length, only_sessions = only_sessions,
- elapsed_threshold = elapsed_threshold)
-
- present_data(data, progress = progress, target_dir = target_dir,
- image_size = image_size, ml_timing = ml_timing)
-
- }, admin = true)
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_status.scala Sat May 06 19:23:33 2017 +0200
@@ -0,0 +1,278 @@
+/* Title: Pure/Admin/build_status.scala
+ Author: Makarius
+
+Present recent build status information from database.
+*/
+
+package isabelle
+
+
+object Build_Status
+{
+ private val default_target_dir = Path.explode("build_status")
+ private val default_history_length = 30
+ private val default_image_size = (800, 600)
+
+
+ /* data profiles */
+
+ sealed case class Profile(name: String, sql: String)
+ {
+ def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
+ {
+ val sql_sessions =
+ if (only_sessions.isEmpty) ""
+ else
+ only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
+ .mkString("(", " OR ", ") AND ")
+
+ Build_Log.Data.universal_table.select(columns, distinct = true,
+ sql = "WHERE " +
+ Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
+ Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
+ " AND " + sql_sessions + SQL.enclose(sql) +
+ " ORDER BY " + Build_Log.Data.pull_date + " DESC")
+ }
+ }
+
+ val standard_profiles: List[Profile] =
+ Jenkins.build_log_profiles :::
+ Isabelle_Cronjob.remote_builds.flatten.toList.map(r => Profile(r.name, r.sql))
+
+ sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
+ {
+ def check(elapsed_threshold: Time): Boolean =
+ !timing.is_zero && timing.elapsed >= elapsed_threshold
+ }
+
+ type Data = Map[String, Map[String, List[Entry]]]
+
+
+ /* read data */
+
+ def read_data(options: Options,
+ profiles: List[Profile] = standard_profiles,
+ progress: Progress = No_Progress,
+ history_length: Int = default_history_length,
+ only_sessions: Set[String] = Set.empty,
+ elapsed_threshold: Time = Time.zero): Data =
+ {
+ var data: Data = Map.empty
+
+ val store = Build_Log.store(options)
+ using(store.open_database())(db =>
+ {
+ for (profile <- profiles) {
+ progress.echo("input " + quote(profile.name))
+ val columns =
+ List(
+ Build_Log.Data.pull_date,
+ Build_Log.Settings.ML_PLATFORM,
+ Build_Log.Data.session_name,
+ Build_Log.Data.threads,
+ Build_Log.Data.timing_elapsed,
+ Build_Log.Data.timing_cpu,
+ Build_Log.Data.timing_gc,
+ Build_Log.Data.ml_timing_elapsed,
+ Build_Log.Data.ml_timing_cpu,
+ Build_Log.Data.ml_timing_gc)
+
+ db.using_statement(profile.select(columns, history_length, only_sessions))(stmt =>
+ {
+ val res = stmt.execute_query()
+ while (res.next()) {
+ val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
+ val threads = res.get_int(Build_Log.Data.threads)
+ val name =
+ profile.name +
+ "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
+ "_M" + threads.getOrElse(1)
+
+ val session = res.string(Build_Log.Data.session_name)
+ val entry =
+ Entry(res.date(Build_Log.Data.pull_date),
+ res.timing(
+ Build_Log.Data.timing_elapsed,
+ Build_Log.Data.timing_cpu,
+ Build_Log.Data.timing_gc),
+ res.timing(
+ Build_Log.Data.ml_timing_elapsed,
+ Build_Log.Data.ml_timing_cpu,
+ Build_Log.Data.ml_timing_gc))
+
+ val session_entries = data.getOrElse(name, Map.empty)
+ val entries = session_entries.getOrElse(session, Nil)
+ data += (name -> (session_entries + (session -> (entry :: entries))))
+ }
+ })
+ }
+ })
+
+ for {
+ (name, session_entries) <- data
+ session_entries1 <-
+ {
+ val session_entries1 =
+ for {
+ (session, entries) <- session_entries
+ if entries.filter(_.check(elapsed_threshold)).length >= 3
+ } yield (session, entries)
+ if (session_entries1.isEmpty) None
+ else Some(session_entries1)
+ }
+ } yield (name, session_entries1)
+ }
+
+
+ /* present data */
+
+ private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
+<html>
+<head><title>Build status</title></head>
+<body>
+"""
+ private val html_footer = """
+</body>
+</html>
+"""
+
+ def present_data(data: Data,
+ progress: Progress = No_Progress,
+ target_dir: Path = default_target_dir,
+ image_size: (Int, Int) = default_image_size,
+ ml_timing: Option[Boolean] = None)
+ {
+ val data_entries = data.toList.sortBy(_._1)
+ for ((name, session_entries) <- data_entries) {
+ val dir = target_dir + Path.explode(name)
+ progress.echo("output " + dir)
+ Isabelle_System.mkdirs(dir)
+
+ for ((session, entries) <- session_entries) {
+ Isabelle_System.with_tmp_file(session, "data") { data_file =>
+ Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
+
+ File.write(data_file,
+ cat_lines(
+ entries.map(entry =>
+ List(entry.date.unix_epoch.toString,
+ entry.timing.elapsed.minutes,
+ entry.timing.cpu.minutes,
+ entry.ml_timing.elapsed.minutes,
+ entry.ml_timing.cpu.minutes,
+ entry.ml_timing.gc.minutes).mkString(" "))))
+
+ val plots1 =
+ List(
+ """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
+ """ using 1:3 smooth csplines title "cpu time" """,
+ """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
+ """ using 1:2 smooth csplines title "elapsed time" """)
+ val plots2 =
+ List(
+ """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
+ """ using 1:5 smooth csplines title "ML cpu time" """,
+ """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
+ """ using 1:4 smooth csplines title "ML elapsed time" """,
+ """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
+ """ using 1:6 smooth csplines title "ML gc time" """)
+ val plots =
+ ml_timing match {
+ case None => plots1
+ case Some(false) => plots1 ::: plots2
+ case Some(true) => plots2
+ }
+
+ File.write(gnuplot_file, """
+set terminal png size """ + image_size._1 + "," + image_size._2 + """
+set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
+set xdata time
+set timefmt "%s"
+set format x "%d-%b"
+set xlabel """ + quote(session) + """ noenhanced
+set key left top
+plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
+
+ val result =
+ Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
+ if (result.rc != 0)
+ result.error("Gnuplot failed for " + name + "/" + session).check
+ }
+ }
+ }
+
+ File.write(dir + Path.basic("index.html"),
+ html_header + "\n<h1>" + HTML.output(name) + "</h1>\n" +
+ cat_lines(
+ session_entries.toList.map(_._1).sorted.map(session =>
+ """<br/><img src=""" + quote(HTML.output(session + ".png")) + """><br/>""")) +
+ "\n" + html_footer)
+ }
+
+ File.write(target_dir + Path.basic("index.html"),
+ html_header + "\n<ul>\n" +
+ cat_lines(
+ data_entries.map(_._1).map(name =>
+ """<li> <a href=""" + quote(HTML.output(name + "/index.html")) + """>""" +
+ HTML.output(name) + """</a> </li>""")) +
+ "\n</ul>\n" + html_footer)
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("build_status", "present recent build status information from database", args =>
+ {
+ var target_dir = default_target_dir
+ var ml_timing: Option[Boolean] = None
+ var only_sessions = Set.empty[String]
+ var elapsed_threshold = Time.zero
+ var history_length = default_history_length
+ var options = Options.init()
+ var image_size = default_image_size
+
+ val getopts = Getopts("""
+Usage: isabelle build_status [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default """ + default_target_dir + """)
+ -M only ML timing
+ -S SESSIONS only given SESSIONS (comma separated)
+ -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
+ -l LENGTH length of history (default """ + default_history_length + """)
+ -m include ML timing
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
+
+ Present performance statistics from build log database, which is specified
+ via system options build_log_database_host, build_log_database_user etc.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "M" -> (_ => ml_timing = Some(true)),
+ "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
+ "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
+ "l:" -> (arg => history_length = Value.Int.parse(arg)),
+ "m" -> (_ => ml_timing = Some(false)),
+ "o:" -> (arg => options = options + arg),
+ "s:" -> (arg =>
+ space_explode('x', arg).map(Value.Int.parse(_)) match {
+ case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
+ case _ => error("Error bad PNG image size: " + quote(arg))
+ }))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress
+
+ val data =
+ read_data(options, profiles = standard_profiles, progress = progress,
+ history_length = history_length, only_sessions = only_sessions,
+ elapsed_threshold = elapsed_threshold)
+
+ present_data(data, progress = progress, target_dir = target_dir,
+ image_size = image_size, ml_timing = ml_timing)
+
+ }, admin = true)
+}
--- a/src/Pure/Admin/jenkins.scala Sat May 06 12:59:16 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala Sat May 06 19:23:33 2017 +0200
@@ -52,9 +52,9 @@
val build_log_jobs = List("isabelle-nightly-benchmark")
- val build_log_profiles: List[Build_Stats.Profile] =
+ val build_log_profiles: List[Build_Status.Profile] =
build_log_jobs.map(job_name =>
- Build_Stats.Profile("jenkins_" + job_name,
+ Build_Status.Profile("jenkins_" + job_name,
Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
--- a/src/Pure/System/isabelle_tool.scala Sat May 06 12:59:16 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sat May 06 19:23:33 2017 +0200
@@ -105,7 +105,7 @@
Build_Docker.isabelle_tool,
Build_JDK.isabelle_tool,
Build_PolyML.isabelle_tool,
- Build_Stats.isabelle_tool,
+ Build_Status.isabelle_tool,
Check_Sources.isabelle_tool,
Doc.isabelle_tool,
Imports.isabelle_tool,
--- a/src/Pure/build-jars Sat May 06 12:59:16 2017 +0200
+++ b/src/Pure/build-jars Sat May 06 19:23:33 2017 +0200
@@ -17,8 +17,8 @@
Admin/build_log.scala
Admin/build_polyml.scala
Admin/build_release.scala
- Admin/build_stats.scala
Admin/build_stats_legacy.scala
+ Admin/build_status.scala
Admin/check_sources.scala
Admin/ci_profile.scala
Admin/isabelle_cronjob.scala