# HG changeset patch
# User wenzelm
# Date 1494097114 -7200
# Node ID 99f4e4e0303022cfa264dd6c03893351bf47831b
# Parent 1019be449dbd4355794557b8949317649d9fe699# Parent 1f4a80e80c8824e0244d2a91af55b17aa4bbaed8
merged
diff -r 1019be449dbd -r 99f4e4e03030 .hgignore
--- 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/
diff -r 1019be449dbd -r 99f4e4e03030 Admin/jenkins/build/ci_build_stats.scala
--- 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(
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/Admin/build_log.scala
--- 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
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/Admin/build_stats.scala
--- 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 = """
-
-Performance statistics from session build output
-
-"""
- private val html_footer = """
-
-
-"""
-
- 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" + HTML.output(job) + "
\n" +
- cat_lines(
- sessions.map(session =>
- """
![]()
""")) +
- "\n" + html_footer)
- }
-
- File.write(target_dir + Path.basic("index.html"),
- html_header + "\n\n" + html_footer)
- }, admin = true)
-}
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/Admin/build_stats_legacy.scala
--- /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
+ }
+}
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/Admin/build_status.scala
--- /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 = """
+
+Build status
+
+"""
+ private val html_footer = """
+
+
+"""
+
+ 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" + HTML.output(name) + "
\n" +
+ cat_lines(
+ session_entries.toList.map(_._1).sorted.map(session =>
+ """
![]()
""")) +
+ "\n" + html_footer)
+ }
+
+ File.write(target_dir + Path.basic("index.html"),
+ html_header + "\n\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)
+}
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/Admin/isabelle_cronjob.scala
--- 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()
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/Admin/jenkins.scala
--- 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(
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/General/date.scala
--- 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
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/General/sql.scala
--- 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")
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/System/isabelle_tool.scala
--- 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,
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/Thy/sessions.scala
--- 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)))
}
})
}
diff -r 1019be449dbd -r 99f4e4e03030 src/Pure/build-jars
--- 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