merged
authorwenzelm
Sat, 06 May 2017 20:58:34 +0200
changeset 65749 99f4e4e03030
parent 65728 1019be449dbd (current diff)
parent 65748 1f4a80e80c88 (diff)
child 65750 7f5556f4b584
merged
src/Pure/Admin/build_stats.scala
--- a/.hgignore	Fri May 05 11:16:13 2017 +0200
+++ b/.hgignore	Sat May 06 20:58:34 2017 +0200
@@ -15,13 +15,9 @@
 ^contrib
 ^heaps/
 ^browser_info/
-^doc/.*\.dvi
-^doc/.*\.eps
 ^doc/.*\.pdf
-^doc/.*\.ps
 ^src/Tools/jEdit/dist/
 ^src/Tools/VSCode/out/
 ^src/Tools/VSCode/extension/node_modules/
 ^src/Tools/VSCode/extension/protocol.log
 ^Admin/jenkins/ci-extras/target/
-^stats/
--- a/Admin/jenkins/build/ci_build_stats.scala	Fri May 05 11:16:13 2017 +0200
+++ b/Admin/jenkins/build/ci_build_stats.scala	Sat May 06 20:58:34 2017 +0200
@@ -26,7 +26,7 @@
     println(s"=== $job ===")
 
     val dir = target_dir + Path.basic(job)
-    val sessions = Build_Stats.present_job(job, dir)
+    val sessions = Build_Stats_Legacy.present_job(job, dir)
 
     val sections =
       cat_lines(
--- a/src/Pure/Admin/build_log.scala	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat May 06 20:58:34 2017 +0200
@@ -11,7 +11,6 @@
 import java.time.ZoneId
 import java.time.format.{DateTimeFormatter, DateTimeParseException}
 import java.util.Locale
-import java.sql.PreparedStatement
 
 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
@@ -687,20 +686,22 @@
         " GROUP BY " + version)
     }
 
+    def recent_time(days: Int): SQL.Source =
+      "now() - INTERVAL '" + days.max(0) + " days'"
+
     def recent_table(days: Int): SQL.Table =
     {
       val table = pull_date_table
       SQL.Table("recent", table.columns,
-        table.select(table.columns) +
-        " WHERE " + pull_date(table) + " > now() - INTERVAL '" + days.max(0) + " days'")
+        table.select(table.columns, "WHERE " + pull_date(table) + " > " + recent_time(days)))
     }
 
     def select_recent(table: SQL.Table, columns: List[SQL.Column], days: Int,
-      distinct: Boolean = false, pull_date: Boolean = false): String =
+      distinct: Boolean = false, pull_date: Boolean = false): SQL.Source =
     {
       val recent = recent_table(days)
       val columns1 = if (pull_date) columns ::: List(Data.pull_date(recent)) else columns
-      table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_alias() +
+      table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_name +
       " ON " + Prop.isabelle_version(table) + " = " + Prop.isabelle_version(recent)
     }
 
@@ -722,7 +723,7 @@
       val columns = aux_columns ::: sessions_table.columns.tail
       SQL.Table("isabelle_build_log", columns,
         {
-          SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_alias() +
+          SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_name +
           " INNER JOIN " + table3 + " ON " + log_name(aux_table) + " = " + log_name(table3)
         })
     }
@@ -779,8 +780,8 @@
             val recent_log_names =
               db.using_statement(
                 Data.select_recent(
-                  Data.meta_info_table, List(Data.log_name), days, distinct = true))(
-                    stmt => SQL.iterator(stmt.executeQuery)(db.string(_, Data.log_name)).toList)
+                  Data.meta_info_table, List(Data.log_name), days, distinct = true))(stmt =>
+                    stmt.execute_query().iterator(_.string(Data.log_name)).toList)
 
             for (log_name <- recent_log_names) {
               read_meta_info(db, log_name).foreach(meta_info =>
@@ -800,11 +801,12 @@
               {
                 db.using_statement(Data.recent_table(days).query)(stmt =>
                 {
-                  val rs = stmt.executeQuery
-                  while (rs.next()) {
-                    for ((c, i) <- table.columns.zipWithIndex)
-                      db2.set_string(stmt2, i + 1, db.get_string(rs, c))
-                    stmt2.execute
+                  val res = stmt.execute_query()
+                  while (res.next()) {
+                    for ((c, i) <- table.columns.zipWithIndex) {
+                      stmt2.string(i + 1) = res.get_string(c)
+                    }
+                    stmt2.execute()
                   }
                 })
               })
@@ -820,19 +822,19 @@
 
     def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
       db.using_statement(table.select(List(column), distinct = true))(stmt =>
-        SQL.iterator(stmt.executeQuery)(db.string(_, column)).toSet)
+        stmt.execute_query().iterator(_.string(column)).toSet)
 
     def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info)
     {
       val table = Data.meta_info_table
       db.using_statement(db.insert_permissive(table))(stmt =>
       {
-        db.set_string(stmt, 1, log_name)
+        stmt.string(1) = log_name
         for ((c, i) <- table.columns.tail.zipWithIndex) {
           if (c.T == SQL.Type.Date)
-            db.set_date(stmt, i + 2, meta_info.get_date(c))
+            stmt.date(i + 2) = meta_info.get_date(c)
           else
-            db.set_string(stmt, i + 2, meta_info.get(c))
+            stmt.string(i + 2) = meta_info.get(c)
         }
         stmt.execute()
       })
@@ -847,21 +849,21 @@
           if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
           else build_info.sessions.iterator
         for ((session_name, session) <- entries_iterator) {
-          db.set_string(stmt, 1, log_name)
-          db.set_string(stmt, 2, session_name)
-          db.set_string(stmt, 3, session.proper_chapter)
-          db.set_string(stmt, 4, session.proper_groups)
-          db.set_int(stmt, 5, session.threads)
-          db.set_long(stmt, 6, session.timing.elapsed.proper_ms)
-          db.set_long(stmt, 7, session.timing.cpu.proper_ms)
-          db.set_long(stmt, 8, session.timing.gc.proper_ms)
-          db.set_double(stmt, 9, session.timing.factor)
-          db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms)
-          db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms)
-          db.set_long(stmt, 12, session.ml_timing.gc.proper_ms)
-          db.set_double(stmt, 13, session.ml_timing.factor)
-          db.set_long(stmt, 14, session.heap_size)
-          db.set_string(stmt, 15, session.status.map(_.toString))
+          stmt.string(1) = log_name
+          stmt.string(2) = session_name
+          stmt.string(3) = session.proper_chapter
+          stmt.string(4) = session.proper_groups
+          stmt.int(5) = session.threads
+          stmt.long(6) = session.timing.elapsed.proper_ms
+          stmt.long(7) = session.timing.cpu.proper_ms
+          stmt.long(8) = session.timing.gc.proper_ms
+          stmt.double(9) = session.timing.factor
+          stmt.long(10) = session.ml_timing.elapsed.proper_ms
+          stmt.long(11) = session.ml_timing.cpu.proper_ms
+          stmt.long(12) = session.ml_timing.gc.proper_ms
+          stmt.double(13) = session.ml_timing.factor
+          stmt.long(14) = session.heap_size
+          stmt.string(15) = session.status.map(_.toString)
           stmt.execute()
         }
       })
@@ -878,9 +880,9 @@
             build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
         val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
         for ((session_name, ml_statistics) <- entries) {
-          db.set_string(stmt, 1, log_name)
-          db.set_string(stmt, 2, session_name)
-          db.set_bytes(stmt, 3, ml_statistics)
+          stmt.string(1) = log_name
+          stmt.string(2) = session_name
+          stmt.bytes(3) = ml_statistics
           stmt.execute()
         }
       })
@@ -934,15 +936,15 @@
       val columns = table.columns.tail
       db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
       {
-        val rs = stmt.executeQuery
-        if (!rs.next) None
+        val res = stmt.execute_query()
+        if (!res.next) None
         else {
           val results =
             columns.map(c => c.name ->
               (if (c.T == SQL.Type.Date)
-                db.get_date(rs, c).map(Log_File.Date_Format(_))
+                res.get_date(c).map(Log_File.Date_Format(_))
                else
-                db.get_string(rs, c)))
+                res.get_string(c)))
           val n = Prop.all_props.length
           val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
           val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
@@ -975,9 +977,9 @@
         if (ml_statistics) {
           val columns = columns1 ::: List(Data.ml_statistics(table2))
           val join =
-            SQL.join_outer(table1, table2,
-              Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
-              Data.session_name(table1) + " = " + Data.session_name(table2))
+            table1 + " LEFT OUTER JOIN " + table2 + " ON " +
+            Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
+            Data.session_name(table1) + " = " + Data.session_name(table2)
           (columns, SQL.enclose(join))
         }
         else (columns1, table1.ident)
@@ -985,26 +987,21 @@
       val sessions =
         db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
         {
-          SQL.iterator(stmt.executeQuery)(rs =>
+          stmt.execute_query().iterator(res =>
           {
-            val session_name = db.string(rs, Data.session_name)
+            val session_name = res.string(Data.session_name)
             val session_entry =
               Session_Entry(
-                chapter = db.string(rs, Data.chapter),
-                groups = split_lines(db.string(rs, Data.groups)),
-                threads = db.get_int(rs, Data.threads),
-                timing =
-                  Timing(Time.ms(db.long(rs, Data.timing_elapsed)),
-                    Time.ms(db.long(rs, Data.timing_cpu)),
-                    Time.ms(db.long(rs, Data.timing_gc))),
+                chapter = res.string(Data.chapter),
+                groups = split_lines(res.string(Data.groups)),
+                threads = res.get_int(Data.threads),
+                timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc),
                 ml_timing =
-                  Timing(Time.ms(db.long(rs, Data.ml_timing_elapsed)),
-                    Time.ms(db.long(rs, Data.ml_timing_cpu)),
-                    Time.ms(db.long(rs, Data.ml_timing_gc))),
-                heap_size = db.get_long(rs, Data.heap_size),
-                status = db.get_string(rs, Data.status).map(Session_Status.withName(_)),
+                  res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc),
+                heap_size = res.get_long(Data.heap_size),
+                status = res.get_string(Data.status).map(Session_Status.withName(_)),
                 ml_statistics =
-                  if (ml_statistics) uncompress_properties(db.bytes(rs, Data.ml_statistics))
+                  if (ml_statistics) uncompress_properties(res.bytes(Data.ml_statistics))
                   else Nil)
             session_name -> session_entry
           }).toMap
--- a/src/Pure/Admin/build_stats.scala	Fri May 05 11:16:13 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-/*  Title:      Pure/Admin/build_stats.scala
-    Author:     Makarius
-
-Statistics from session build output.
-*/
-
-package isabelle
-
-
-object Build_Stats
-{
-  /* presentation */
-
-  private val default_history_length = 100
-  private val default_size = (800, 600)
-  private val default_only_sessions = Set.empty[String]
-  private val default_elapsed_threshold = Time.zero
-  private val default_ml_timing: Option[Boolean] = None
-
-  def present_job(job: String, dir: Path,
-    history_length: Int = default_history_length,
-    size: (Int, Int) = default_size,
-    only_sessions: Set[String] = default_only_sessions,
-    elapsed_threshold: Time = default_elapsed_threshold,
-    ml_timing: Option[Boolean] = default_ml_timing): List[String] =
-  {
-    val job_infos = Jenkins.build_job_infos(job).take(history_length)
-    if (job_infos.isEmpty) error("No build infos for job " + quote(job))
-
-    val all_infos =
-      Par_List.map((info: Jenkins.Job_Info) =>
-        {
-          val t = info.timestamp / 1000
-          val log_file = Build_Log.Log_File(info.log_filename.implode, Url.read(info.main_log))
-          (t, log_file.parse_build_info())
-        }, job_infos)
-    val all_sessions =
-      (Set.empty[String] /: all_infos)(
-        { case (s, (_, info)) => s ++ info.sessions.keySet })
-
-    def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
-    {
-      val t = info.timing(session)
-      !t.is_zero && t.elapsed >= elapsed_threshold
-    }
-
-    val sessions =
-      for {
-        session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
-        if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
-      } yield session
-
-    Isabelle_System.mkdirs(dir)
-    for (session <- sessions) {
-      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(session) }
-            yield {
-              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))
-
-          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(plot_file, """
-set terminal png size """ + size._1 + "," + 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(plot_file))
-          if (result.rc != 0) {
-            Output.error_message("Session " + session + ": gnuplot error")
-            result.print
-          }
-        }
-      }
-    }
-
-    sessions.toList.sorted
-  }
-
-
-  /* Isabelle tool wrapper */
-
-  private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
-<head><title>Performance statistics from session build output</title></head>
-<body>
-"""
-  private val html_footer = """
-</body>
-</html>
-"""
-
-  val isabelle_tool =
-    Isabelle_Tool("build_stats", "present statistics from session build output", args =>
-    {
-      var target_dir = Path.explode("stats")
-      var ml_timing = default_ml_timing
-      var only_sessions = default_only_sessions
-      var elapsed_threshold = default_elapsed_threshold
-      var history_length = default_history_length
-      var size = default_size
-
-      val getopts = Getopts("""
-Usage: isabelle build_stats [OPTIONS] [JOBS ...]
-
-  Options are:
-    -D DIR       target directory (default "stats")
-    -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 100)
-    -m           include ML timing
-    -s WxH       size of PNG image (default 800x600)
-
-  Present statistics from session build output of the given JOBS, from Jenkins
-  continuous build service specified as URL via ISABELLE_JENKINS_ROOT.
-""",
-        "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)),
-        "s:" -> (arg =>
-          space_explode('x', arg).map(Value.Int.parse(_)) match {
-            case List(w, h) if w > 0 && h > 0 => size = (w, h)
-            case _ => error("Error bad PNG image size: " + quote(arg))
-          }))
-
-      val jobs = getopts(args)
-      val all_jobs = Jenkins.build_job_names()
-      val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
-
-      if (jobs.isEmpty)
-        error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
-
-      if (bad_jobs.nonEmpty)
-        error("Unknown build jobs: " + bad_jobs.mkString(" ") +
-          "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
-
-      for (job <- jobs) {
-        val dir = target_dir + Path.basic(job)
-        Output.writeln(dir.implode)
-        val sessions =
-          present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing)
-        File.write(dir + Path.basic("index.html"),
-          html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" +
-          cat_lines(
-            sessions.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(
-          jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" +
-            HTML.output(job) + """</a> </li>""")) +
-        "\n</ul>\n" + html_footer)
-  }, admin = true)
-}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_stats_legacy.scala	Sat May 06 20:58:34 2017 +0200
@@ -0,0 +1,111 @@
+/*  Title:      Pure/Admin/build_stats_legacy.scala
+    Author:     Makarius
+
+Statistics from session build output.
+*/
+
+package isabelle
+
+
+object Build_Stats_Legacy
+{
+  /* presentation */
+
+  private val default_history_length = 100
+  private val default_size = (800, 600)
+  private val default_only_sessions = Set.empty[String]
+  private val default_elapsed_threshold = Time.zero
+  private val default_ml_timing: Option[Boolean] = None
+
+  def present_job(job: String, dir: Path,
+    history_length: Int = default_history_length,
+    size: (Int, Int) = default_size,
+    only_sessions: Set[String] = default_only_sessions,
+    elapsed_threshold: Time = default_elapsed_threshold,
+    ml_timing: Option[Boolean] = default_ml_timing): List[String] =
+  {
+    val job_infos = Jenkins.build_job_infos(job).take(history_length)
+    if (job_infos.isEmpty) error("No build infos for job " + quote(job))
+
+    val all_infos =
+      Par_List.map((info: Jenkins.Job_Info) =>
+        {
+          val log_file = Build_Log.Log_File(info.log_filename.implode, Url.read(info.main_log))
+          (info.date, log_file.parse_build_info())
+        }, job_infos)
+    val all_sessions =
+      (Set.empty[String] /: all_infos)(
+        { case (s, (_, info)) => s ++ info.sessions.keySet })
+
+    def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
+    {
+      val t = info.timing(session)
+      !t.is_zero && t.elapsed >= elapsed_threshold
+    }
+
+    val sessions =
+      for {
+        session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
+        if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
+      } yield session
+
+    Isabelle_System.mkdirs(dir)
+    for (session <- sessions) {
+      Isabelle_System.with_tmp_file(session, "png") { data_file =>
+        Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
+          val data =
+            for { (date, info) <- all_infos if info.finished(session) }
+            yield {
+              val timing1 = info.timing(session)
+              val timing2 = info.ml_timing(session)
+              List(date.unix_epoch.toString,
+                timing1.elapsed.minutes,
+                timing1.cpu.minutes,
+                timing2.elapsed.minutes,
+                timing2.cpu.minutes,
+                timing2.gc.minutes).mkString(" ")
+            }
+          File.write(data_file, cat_lines(data))
+
+          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(plot_file, """
+set terminal png size """ + size._1 + "," + 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(plot_file))
+          if (result.rc != 0) {
+            Output.error_message("Session " + session + ": gnuplot error")
+            result.print
+          }
+        }
+      }
+    }
+
+    sessions.toList.sorted
+  }
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_status.scala	Sat May 06 20:58:34 2017 +0200
@@ -0,0 +1,276 @@
+/*  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_status_profiles ::: Isabelle_Cronjob.build_status_profiles
+
+  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, 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/isabelle_cronjob.scala	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat May 06 20:58:34 2017 +0200
@@ -29,10 +29,11 @@
   val afp_source = "https://bitbucket.org/isa-afp/afp-devel"
 
   val devel_dir = Path.explode("~/html-data/devel")
-  val release_snapshot = devel_dir + Path.explode("release_snapshot")
-  val build_log_snapshot = devel_dir + Path.explode("build_log.db")
+  val release_snapshot_dir = devel_dir + Path.explode("release_snapshot")
+  val build_log_db = devel_dir + Path.explode("build_log.db")
+  val build_status_dir = devel_dir + Path.explode("build_status")
 
-  val jenkins_jobs = List("isabelle-nightly-benchmark", "identify")
+  val jenkins_jobs = "identify" :: Jenkins.build_log_jobs
 
 
 
@@ -50,8 +51,8 @@
           File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
             Build_Log.Identify.content(logger.start_date, Some(rev), Some(afp_rev)))
 
-          val new_snapshot = release_snapshot.ext("new")
-          val old_snapshot = release_snapshot.ext("old")
+          val new_snapshot = release_snapshot_dir.ext("new")
+          val old_snapshot = release_snapshot_dir.ext("old")
 
           Isabelle_System.rm_tree(new_snapshot)
           Isabelle_System.rm_tree(old_snapshot)
@@ -59,8 +60,8 @@
           Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
             parallel_jobs = 4, remote_mac = "macbroy31", website = Some(new_snapshot))
 
-          if (release_snapshot.is_dir) File.move(release_snapshot, old_snapshot)
-          File.move(new_snapshot, release_snapshot)
+          if (release_snapshot_dir.is_dir) File.move(release_snapshot_dir, old_snapshot)
+          File.move(new_snapshot, release_snapshot_dir)
           Isabelle_System.rm_tree(old_snapshot)
         }))
 
@@ -87,29 +88,55 @@
   /* remote build_history */
 
   sealed case class Remote_Build(
+    name: String,
     host: String,
     user: String = "",
     port: Int = 0,
     shared_home: Boolean = true,
     options: String = "",
-    args: String = "")
+    args: String = "",
+    detect: SQL.Source = "")
+  {
+    def profile: Build_Status.Profile =
+    {
+      val sql =
+        Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
+        Build_Log.Prop.build_host + " = " + SQL.string(host) +
+        (if (detect == "") "" else " AND " + SQL.enclose(detect))
+      Build_Status.Profile(name, sql)
+    }
+  }
 
-  private val remote_builds =
+  private val remote_builds: List[List[Remote_Build]] =
+  {
     List(
-      List(Remote_Build("lxbroy8",
+      List(Remote_Build("polyml-test", "lxbroy8",
         options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
-        args = "-N -g timing")),
-      List(Remote_Build("lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")),
-      List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
+        args = "-N -g timing",
+        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test"))),
+      List(Remote_Build("linux1", "lxbroy9",
+        options = "-m32 -B -M1x2,2", args = "-N -g timing")),
+      List(Remote_Build("linux2", "lxbroy10",
+        options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
       List(
-        Remote_Build("macbroy2", options = "-m32 -M8", args = "-a"),
-        Remote_Build("macbroy2", options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty"),
-        Remote_Build("macbroy2", options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs")),
-      List(Remote_Build("macbroy30", options = "-m32 -M2", args = "-a")),
-      List(Remote_Build("macbroy31", options = "-m32 -M2", args = "-a")),
+        Remote_Build("macos1", "macbroy2", options = "-m32 -M8", args = "-a",
+          detect = Build_Log.Prop.build_tags + " IS NULL"),
+        Remote_Build("macos1_quick_and_dirty", "macbroy2",
+          options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
+          detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")),
+        Remote_Build("macos1_skip_proofs", "macbroy2",
+          options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
+          detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"))),
+      List(Remote_Build("macos2", "macbroy30", options = "-m32 -M2", args = "-a")),
+      List(Remote_Build("macos3", "macbroy31", options = "-m32 -M2", args = "-a")),
       List(
-        Remote_Build("vmnipkow9", shared_home = false, options = "-m32 -M4", args = "-a"),
-        Remote_Build("vmnipkow9", shared_home = false, options = "-m64 -M4", args = "-a")))
+        Remote_Build("windows", "vmnipkow9", shared_home = false,
+          options = "-m32 -M4", args = "-a",
+          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
+        Remote_Build("windows", "vmnipkow9", shared_home = false,
+          options = "-m64 -M4", args = "-a",
+          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
+  }
 
   private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
   {
@@ -153,11 +180,22 @@
     using(store.open_database())(db =>
     {
       store.update_database(db, database_dirs, ml_statistics = true)
-      store.snapshot_database(db, build_log_snapshot)
+      store.snapshot_database(db, build_log_db)
     })
   }
 
 
+  /* present build status */
+
+  val build_status_profiles: List[Build_Status.Profile] =
+    remote_builds.flatten.map(_.profile)
+
+  def build_status(options: Options)
+  {
+    Build_Status.present_data(Build_Status.read_data(options), target_dir = build_status_dir)
+  }
+
+
 
   /** task logging **/
 
@@ -304,7 +342,8 @@
           SEQ(List(build_release, build_history_base,
             PAR(remote_builds.map(seq => SEQ(seq.map(remote_build_history(rev, _))))),
             Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
-            Logger_Task("build_log_database", logger => database_update(logger.options)))))))
+            Logger_Task("build_log_database", logger => database_update(logger.options)),
+            Logger_Task("build_status", logger => build_status(logger.options)))))))
 
     log_service.shutdown()
 
--- a/src/Pure/Admin/jenkins.scala	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala	Sat May 06 20:58:34 2017 +0200
@@ -48,6 +48,17 @@
   }
 
 
+  /* build log status */
+
+  val build_log_jobs = List("isabelle-nightly-benchmark")
+
+  val build_status_profiles: List[Build_Status.Profile] =
+    build_log_jobs.map(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)))
+
+
   /* job info */
 
   sealed case class Job_Info(
--- a/src/Pure/General/date.scala	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/General/date.scala	Sat May 06 20:58:34 2017 +0200
@@ -93,6 +93,7 @@
   def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
   def to_utc: Date = to(ZoneId.of("UTC"))
 
+  def unix_epoch: Long = rep.toEpochSecond
   def instant: Instant = Instant.from(rep)
   def time: Time = Time.instant(instant)
   def timezone: ZoneId = rep.getZone
--- a/src/Pure/General/sql.scala	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/General/sql.scala	Sat May 06 20:58:34 2017 +0200
@@ -9,11 +9,16 @@
 import java.time.OffsetDateTime
 import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet}
 
+import scala.collection.mutable
+
 
 object SQL
 {
   /** SQL language **/
 
+  type Source = String
+
+
   /* concrete syntax */
 
   def escape_char(c: Char): String =
@@ -30,24 +35,17 @@
       case _ => c.toString
     }
 
-  def string(s: String): String =
+  def string(s: String): Source =
     "'" + s.map(escape_char(_)).mkString + "'"
 
-  def ident(s: String): String =
+  def ident(s: String): Source =
     Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))
 
-  def enclose(s: String): String = "(" + s + ")"
-  def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")
-
-  def select(columns: List[Column], distinct: Boolean = false): String =
-    "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.ident)) + " FROM "
+  def enclose(s: Source): Source = "(" + s + ")"
+  def enclosure(ss: Iterable[Source]): Source = ss.mkString("(", ", ", ")")
 
-  def join(table1: Table, table2: Table, sql: String = "", outer: Boolean = false): String =
-    table1.ident + (if (outer) " LEFT OUTER JOIN " else " INNER JOIN ") + table2.ident +
-      (if (sql == "") "" else " ON " + sql)
-
-  def join_outer(table1: Table, table2: Table, sql: String = ""): String =
-    join(table1, table2, sql, outer = true)
+  def select(columns: List[Column], distinct: Boolean = false): Source =
+    "SELECT " + (if (distinct) "DISTINCT " else "") + commas(columns.map(_.ident)) + " FROM "
 
 
   /* types */
@@ -63,14 +61,14 @@
     val Date = Value("TIMESTAMP WITH TIME ZONE")
   }
 
-  def sql_type_default(T: Type.Value): String = T.toString
+  def sql_type_default(T: Type.Value): Source = T.toString
 
-  def sql_type_sqlite(T: Type.Value): String =
+  def sql_type_sqlite(T: Type.Value): Source =
     if (T == Type.Boolean) "INTEGER"
     else if (T == Type.Date) "TEXT"
     else sql_type_default(T)
 
-  def sql_type_postgresql(T: Type.Value): String =
+  def sql_type_postgresql(T: Type.Value): Source =
     if (T == Type.Bytes) "BYTEA"
     else sql_type_default(T)
 
@@ -101,20 +99,20 @@
     def apply(table: Table): Column =
       Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
-    def ident: String = SQL.ident(name)
+    def ident: Source = SQL.ident(name)
 
-    def decl(sql_type: Type.Value => String): String =
+    def decl(sql_type: Type.Value => Source): Source =
       ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
-    def where_equal(s: String): String = "WHERE " + ident + " = " + string(s)
+    def where_equal(s: String): Source = "WHERE " + ident + " = " + string(s)
 
-    override def toString: String = ident
+    override def toString: Source = ident
   }
 
 
   /* tables */
 
-  sealed case class Table(name: String, columns: List[Column], body: String = "")
+  sealed case class Table(name: String, columns: List[Column], body: Source = "")
   {
     private val columns_index: Map[String, Int] =
       columns.iterator.map(_.name).zipWithIndex.toMap
@@ -124,16 +122,15 @@
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
     }
 
-    def ident: String = SQL.ident(name)
+    def ident: Source = SQL.ident(name)
 
-    def query: String =
+    def query: Source =
       if (body == "") error("Missing SQL body for table " + quote(name))
       else SQL.enclose(body)
 
-    def query_alias(alias: String = name): String =
-      query + " AS " + SQL.ident(alias)
+    def query_name: Source = query + " AS " + SQL.ident(name)
 
-    def create(strict: Boolean = false, sql_type: Type.Value => String): String =
+    def create(strict: Boolean = false, sql_type: Type.Value => Source): Source =
     {
       val primary_key =
         columns.filter(_.primary_key).map(_.name) match {
@@ -145,46 +142,160 @@
     }
 
     def create_index(index_name: String, index_columns: List[Column],
-        strict: Boolean = false, unique: Boolean = false): String =
+        strict: Boolean = false, unique: Boolean = false): Source =
       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
         ident + " " + enclosure(index_columns.map(_.name))
 
-    def insert_cmd(cmd: String, sql: String = ""): String =
+    def insert_cmd(cmd: Source, sql: Source = ""): Source =
       cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
         (if (sql == "") "" else " " + sql)
 
-    def insert(sql: String = ""): String = insert_cmd("INSERT", sql)
+    def insert(sql: Source = ""): Source = insert_cmd("INSERT", sql)
 
-    def delete(sql: String = ""): String =
+    def delete(sql: Source = ""): Source =
       "DELETE FROM " + ident +
         (if (sql == "") "" else " " + sql)
 
-    def select(select_columns: List[Column], sql: String = "", distinct: Boolean = false): String =
+    def select(select_columns: List[Column], sql: Source = "", distinct: Boolean = false): Source =
       SQL.select(select_columns, distinct = distinct) + ident +
         (if (sql == "") "" else " " + sql)
 
-    override def toString: String = ident
+    override def toString: Source = ident
   }
 
 
 
   /** SQL database operations **/
 
+  /* statements */
+
+  class Statement private[SQL](val db: Database, val rep: PreparedStatement)
+  {
+    stmt =>
+
+    object bool
+    {
+      def update(i: Int, x: Boolean) { rep.setBoolean(i, x) }
+      def update(i: Int, x: Option[Boolean])
+      {
+        if (x.isDefined) update(i, x.get)
+        else rep.setNull(i, java.sql.Types.BOOLEAN)
+      }
+    }
+    object int
+    {
+      def update(i: Int, x: Int) { rep.setInt(i, x) }
+      def update(i: Int, x: Option[Int])
+      {
+        if (x.isDefined) update(i, x.get)
+        else rep.setNull(i, java.sql.Types.INTEGER)
+      }
+    }
+    object long
+    {
+      def update(i: Int, x: Long) { rep.setLong(i, x) }
+      def update(i: Int, x: Option[Long])
+      {
+        if (x.isDefined) update(i, x.get)
+        else rep.setNull(i, java.sql.Types.BIGINT)
+      }
+    }
+    object double
+    {
+      def update(i: Int, x: Double) { rep.setDouble(i, x) }
+      def update(i: Int, x: Option[Double])
+      {
+        if (x.isDefined) update(i, x.get)
+        else rep.setNull(i, java.sql.Types.DOUBLE)
+      }
+    }
+    object string
+    {
+      def update(i: Int, x: String) { rep.setString(i, x) }
+      def update(i: Int, x: Option[String]): Unit = update(i, x.orNull)
+    }
+    object bytes
+    {
+      def update(i: Int, bytes: Bytes)
+      {
+        if (bytes == null) rep.setBytes(i, null)
+        else rep.setBinaryStream(i, bytes.stream(), bytes.length)
+      }
+      def update(i: Int, bytes: Option[Bytes]): Unit = update(i, bytes.orNull)
+    }
+    object date
+    {
+      def update(i: Int, date: Date): Unit = db.update_date(stmt, i, date)
+      def update(i: Int, date: Option[Date]): Unit = update(i, date.orNull)
+    }
+
+    def execute(): Boolean = rep.execute()
+    def execute_query(): Result = new Result(this, rep.executeQuery())
+
+    def close(): Unit = rep.close
+  }
+
+
   /* results */
 
-  def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
+  class Result private[SQL](val stmt: Statement, val rep: ResultSet)
   {
-    private var _next: Boolean = rs.next()
-    def hasNext: Boolean = _next
-    def next: A = { val x = get(rs); _next = rs.next(); x }
+    res =>
+
+    def next(): Boolean = rep.next()
+
+    def iterator[A](get: Result => A): Iterator[A] = new Iterator[A]
+    {
+      private var _next: Boolean = res.next()
+      def hasNext: Boolean = _next
+      def next: A = { val x = get(res); _next = res.next(); x }
+    }
+
+    def bool(column: Column): Boolean = rep.getBoolean(column.name)
+    def int(column: Column): Int = rep.getInt(column.name)
+    def long(column: Column): Long = rep.getLong(column.name)
+    def double(column: Column): Double = rep.getDouble(column.name)
+    def string(column: Column): String =
+    {
+      val s = rep.getString(column.name)
+      if (s == null) "" else s
+    }
+    def bytes(column: Column): Bytes =
+    {
+      val bs = rep.getBytes(column.name)
+      if (bs == null) Bytes.empty else Bytes(bs)
+    }
+    def date(column: Column): Date = stmt.db.date(res, column)
+
+    def timing(c1: Column, c2: Column, c3: Column) =
+      Timing(Time.ms(long(c1)), Time.ms(long(c2)), Time.ms(long(c3)))
+
+    def get[A](column: Column, f: Column => A): Option[A] =
+    {
+      val x = f(column)
+      if (rep.wasNull) None else Some(x)
+    }
+    def get_bool(column: Column): Option[Boolean] = get(column, bool _)
+    def get_int(column: Column): Option[Int] = get(column, int _)
+    def get_long(column: Column): Option[Long] = get(column, long _)
+    def get_double(column: Column): Option[Double] = get(column, double _)
+    def get_string(column: Column): Option[String] = get(column, string _)
+    def get_bytes(column: Column): Option[Bytes] = get(column, bytes _)
+    def get_date(column: Column): Option[Date] = get(column, date _)
   }
 
+
+  /* database */
+
   trait Database
   {
+    db =>
+
+
     /* types */
 
-    def sql_type(T: Type.Value): String
+    def sql_type(T: Type.Value): Source
 
 
     /* connection */
@@ -210,102 +321,31 @@
     }
 
 
-    /* statements */
+    /* statements and results */
 
-    def statement(sql: String): PreparedStatement =
-      connection.prepareStatement(sql)
+    def statement(sql: Source): Statement =
+      new Statement(db, connection.prepareStatement(sql))
 
-    def using_statement[A](sql: String)(f: PreparedStatement => A): A =
+    def using_statement[A](sql: Source)(f: Statement => A): A =
       using(statement(sql))(f)
 
-    def insert_permissive(table: Table, sql: String = ""): String
-
-
-    /* input */
-
-    def set_bool(stmt: PreparedStatement, i: Int, x: Boolean) { stmt.setBoolean(i, x) }
-    def set_bool(stmt: PreparedStatement, i: Int, x: Option[Boolean])
-    {
-      if (x.isDefined) set_bool(stmt, i, x.get)
-      else stmt.setNull(i, java.sql.Types.BOOLEAN)
-    }
-
-    def set_int(stmt: PreparedStatement, i: Int, x: Int) { stmt.setInt(i, x) }
-    def set_int(stmt: PreparedStatement, i: Int, x: Option[Int])
-    {
-      if (x.isDefined) set_int(stmt, i, x.get)
-      else stmt.setNull(i, java.sql.Types.INTEGER)
-    }
-
-    def set_long(stmt: PreparedStatement, i: Int, x: Long) { stmt.setLong(i, x) }
-    def set_long(stmt: PreparedStatement, i: Int, x: Option[Long])
-    {
-      if (x.isDefined) set_long(stmt, i, x.get)
-      else stmt.setNull(i, java.sql.Types.BIGINT)
-    }
-
-    def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) }
-    def set_double(stmt: PreparedStatement, i: Int, x: Option[Double])
-    {
-      if (x.isDefined) set_double(stmt, i, x.get)
-      else stmt.setNull(i, java.sql.Types.DOUBLE)
-    }
-
-    def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) }
-    def set_string(stmt: PreparedStatement, i: Int, x: Option[String]): Unit =
-      set_string(stmt, i, x.orNull)
+    def update_date(stmt: Statement, i: Int, date: Date): Unit
+    def date(res: Result, column: Column): Date
 
-    def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes)
-    {
-      if (bytes == null) stmt.setBytes(i, null)
-      else stmt.setBinaryStream(i, bytes.stream(), bytes.length)
-    }
-    def set_bytes(stmt: PreparedStatement, i: Int, bytes: Option[Bytes]): Unit =
-      set_bytes(stmt, i, bytes.orNull)
-
-    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit
-    def set_date(stmt: PreparedStatement, i: Int, date: Option[Date]): Unit =
-      set_date(stmt, i, date.orNull)
-
-
-    /* output */
-
-    def bool(rs: ResultSet, column: Column): Boolean = rs.getBoolean(column.name)
-    def int(rs: ResultSet, column: Column): Int = rs.getInt(column.name)
-    def long(rs: ResultSet, column: Column): Long = rs.getLong(column.name)
-    def double(rs: ResultSet, column: Column): Double = rs.getDouble(column.name)
-    def string(rs: ResultSet, column: Column): String =
-    {
-      val s = rs.getString(column.name)
-      if (s == null) "" else s
-    }
-    def bytes(rs: ResultSet, column: Column): Bytes =
-    {
-      val bs = rs.getBytes(column.name)
-      if (bs == null) Bytes.empty else Bytes(bs)
-    }
-    def date(rs: ResultSet, column: Column): Date
-
-    def get[A](rs: ResultSet, column: Column, f: (ResultSet, Column) => A): Option[A] =
-    {
-      val x = f(rs, column)
-      if (rs.wasNull) None else Some(x)
-    }
-    def get_bool(rs: ResultSet, column: Column): Option[Boolean] = get(rs, column, bool _)
-    def get_int(rs: ResultSet, column: Column): Option[Int] = get(rs, column, int _)
-    def get_long(rs: ResultSet, column: Column): Option[Long] = get(rs, column, long _)
-    def get_double(rs: ResultSet, column: Column): Option[Double] = get(rs, column, double _)
-    def get_string(rs: ResultSet, column: Column): Option[String] = get(rs, column, string _)
-    def get_bytes(rs: ResultSet, column: Column): Option[Bytes] = get(rs, column, bytes _)
-    def get_date(rs: ResultSet, column: Column): Option[Date] = get(rs, column, date _)
+    def insert_permissive(table: Table, sql: Source = ""): Source
 
 
     /* tables and views */
 
     def tables: List[String] =
-      iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
+    {
+      val result = new mutable.ListBuffer[String]
+      val rs = connection.getMetaData.getTables(null, null, "%", null)
+      while (rs.next) { result += rs.getString(3) }
+      result.toList
+    }
 
-    def create_table(table: Table, strict: Boolean = false, sql: String = ""): Unit =
+    def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
       using_statement(
         table.create(strict, sql_type) + (if (sql == "") "" else " " + sql))(_.execute())
 
@@ -316,7 +356,7 @@
     def create_view(table: Table, strict: Boolean = false): Unit =
     {
       if (strict || !tables.contains(table.name)) {
-        val sql = "CREATE VIEW " + table.ident + " AS " + { table.query; table.body }
+        val sql = "CREATE VIEW " + table + " AS " + { table.query; table.body }
         using_statement(sql)(_.execute())
       }
     }
@@ -348,16 +388,16 @@
   {
     override def toString: String = name
 
-    def sql_type(T: SQL.Type.Value): String = SQL.sql_type_sqlite(T)
+    def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
 
-    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
-      if (date == null) set_string(stmt, i, null: String)
-      else set_string(stmt, i, date_format(date))
+    def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
+      if (date == null) stmt.string(i) = (null: String)
+      else stmt.string(i) = date_format(date)
 
-    def date(rs: ResultSet, column: SQL.Column): Date =
-      date_format.parse(string(rs, column))
+    def date(res: SQL.Result, column: SQL.Column): Date =
+      date_format.parse(res.string(column))
 
-    def insert_permissive(table: SQL.Table, sql: String = ""): String =
+    def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd("INSERT OR IGNORE", sql = sql)
 
     def rebuild { using_statement("VACUUM")(_.execute()) }
@@ -420,20 +460,20 @@
   {
     override def toString: String = name
 
-    def sql_type(T: SQL.Type.Value): String = SQL.sql_type_postgresql(T)
+    def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
 
     // see https://jdbc.postgresql.org/documentation/head/8-date-time.html
-    def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit =
-      if (date == null) stmt.setObject(i, null)
-      else stmt.setObject(i, OffsetDateTime.from(date.to_utc.rep))
+    def update_date(stmt: SQL.Statement, i: Int, date: Date): Unit =
+      if (date == null) stmt.rep.setObject(i, null)
+      else stmt.rep.setObject(i, OffsetDateTime.from(date.to_utc.rep))
 
-    def date(rs: ResultSet, column: SQL.Column): Date =
+    def date(res: SQL.Result, column: SQL.Column): Date =
     {
-      val obj = rs.getObject(column.name, classOf[OffsetDateTime])
+      val obj = res.rep.getObject(column.name, classOf[OffsetDateTime])
       if (obj == null) null else Date.instant(obj.toInstant)
     }
 
-    def insert_permissive(table: SQL.Table, sql: String = ""): String =
+    def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
       table.insert_cmd("INSERT",
         sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
 
--- a/src/Pure/System/isabelle_tool.scala	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sat May 06 20:58:34 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/Thy/sessions.scala	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat May 06 20:58:34 2017 +0200
@@ -10,7 +10,6 @@
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
-import java.sql.PreparedStatement
 
 import scala.collection.SortedSet
 import scala.collection.mutable
@@ -766,8 +765,8 @@
       db.using_statement(Session_Info.table.select(List(column),
         Session_Info.session_name.where_equal(name)))(stmt =>
       {
-        val rs = stmt.executeQuery
-        if (!rs.next) Bytes.empty else db.bytes(rs, column)
+        val res = stmt.execute_query()
+        if (!res.next()) Bytes.empty else res.bytes(column)
       })
 
     def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
@@ -825,15 +824,15 @@
           Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
         db.using_statement(Session_Info.table.insert())(stmt =>
         {
-          db.set_string(stmt, 1, name)
-          db.set_bytes(stmt, 2, encode_properties(build_log.session_timing))
-          db.set_bytes(stmt, 3, compress_properties(build_log.command_timings))
-          db.set_bytes(stmt, 4, compress_properties(build_log.ml_statistics))
-          db.set_bytes(stmt, 5, compress_properties(build_log.task_statistics))
-          db.set_string(stmt, 6, cat_lines(build.sources))
-          db.set_string(stmt, 7, cat_lines(build.input_heaps))
-          db.set_string(stmt, 8, build.output_heap getOrElse "")
-          db.set_int(stmt, 9, build.return_code)
+          stmt.string(1) = name
+          stmt.bytes(2) = encode_properties(build_log.session_timing)
+          stmt.bytes(3) = compress_properties(build_log.command_timings)
+          stmt.bytes(4) = compress_properties(build_log.ml_statistics)
+          stmt.bytes(5) = compress_properties(build_log.task_statistics)
+          stmt.string(6) = cat_lines(build.sources)
+          stmt.string(7) = cat_lines(build.input_heaps)
+          stmt.string(8) = build.output_heap getOrElse ""
+          stmt.int(9) = build.return_code
           stmt.execute()
         })
       }
@@ -867,15 +866,15 @@
       db.using_statement(Session_Info.table.select(Session_Info.build_columns,
         Session_Info.session_name.where_equal(name)))(stmt =>
       {
-        val rs = stmt.executeQuery
-        if (!rs.next) None
+        val res = stmt.execute_query()
+        if (!res.next()) None
         else {
           Some(
             Build.Session_Info(
-              split_lines(db.string(rs, Session_Info.sources)),
-              split_lines(db.string(rs, Session_Info.input_heaps)),
-              db.string(rs, Session_Info.output_heap) match { case "" => None case s => Some(s) },
-              db.int(rs, Session_Info.return_code)))
+              split_lines(res.string(Session_Info.sources)),
+              split_lines(res.string(Session_Info.input_heaps)),
+              res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
+              res.int(Session_Info.return_code)))
         }
       })
   }
--- a/src/Pure/build-jars	Fri May 05 11:16:13 2017 +0200
+++ b/src/Pure/build-jars	Sat May 06 20:58:34 2017 +0200
@@ -17,7 +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