--- a/src/Pure/Admin/build_log.scala Wed Oct 18 11:53:01 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Wed Oct 18 19:53:19 2017 +0200
@@ -736,7 +736,9 @@
/* earliest pull date for repository version (PostgreSQL queries) */
- val pull_date = SQL.Column.date("pull_date")
+ def pull_date(afp: Boolean = false) =
+ if (afp) SQL.Column.date("afp_pull_date")
+ else SQL.Column.date("pull_date")
def pull_date_table(afp: Boolean = false): SQL.Table =
{
@@ -744,8 +746,9 @@
if (afp) ("afp_pull_date", List(Prop.isabelle_version, Prop.afp_version))
else ("pull_date", List(Prop.isabelle_version))
- build_log_table(name, versions.map(_.make_primary_key) ::: List(pull_date),
- "SELECT " + versions.mkString(", ") + ", min(" + Prop.build_start + ") AS " + pull_date +
+ build_log_table(name, versions.map(_.make_primary_key) ::: List(pull_date(afp)),
+ "SELECT " + versions.mkString(", ") +
+ ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
" FROM " + meta_info_table +
" WHERE " + (versions ::: List(Prop.build_start)).map(_.defined).mkString(" AND ") +
" GROUP BY " + versions.mkString(", "))
@@ -771,7 +774,7 @@
SQL.Table("recent_pull_date", table.columns,
table.select(table.columns,
- "WHERE " + pull_date(table) + " > " + recent_time(days) +
+ "WHERE " + pull_date(afp)(table) + " > " + recent_time(days) +
(if (rev != "" && rev2 == "") " OR " + eq1
else if (rev == "" && rev2 != "") " OR " + eq2
else if (rev != "" && rev2 != "") " OR (" + eq1 + " AND " + eq2 + ")"
@@ -789,6 +792,7 @@
def select_recent_versions(days: Int,
rev: String = "", afp_rev: Option[String] = None, sql: SQL.Source = ""): SQL.Source =
{
+ val afp = afp_rev.isDefined
val version = Prop.isabelle_version
val table1 = recent_pull_date_table(days, rev = rev, afp_rev = afp_rev)
val table2 = meta_info_table
@@ -800,7 +804,7 @@
SQL.select(columns, distinct = true) +
table1.query_named + SQL.join_outer + aux_table.query_named +
" ON " + version(table1) + " = " + version(aux_table) +
- " ORDER BY " + pull_date(table1) + " DESC"
+ " ORDER BY " + pull_date(afp)(table1) + " DESC"
}
@@ -808,30 +812,42 @@
val universal_table: SQL.Table =
{
+ val afp_pull_date = pull_date(afp = true)
+ val version1 = Prop.isabelle_version
+ val version2 = Prop.afp_version
val table1 = meta_info_table
- val table2 = pull_date_table()
- val table3 = sessions_table
- val table4 = ml_statistics_table
+ val table2 = pull_date_table(afp = true)
+ val table3 = pull_date_table()
- val a_columns = log_name :: pull_date :: meta_info_table.columns.tail
+ val a_columns = log_name :: afp_pull_date :: table1.columns.tail
val a_table =
SQL.Table("a", a_columns,
- SQL.select(a_columns.take(2) ::: a_columns.drop(2).map(_.apply(table1))) +
- table1 + SQL.join_outer + table2 + " ON " +
- Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2))
+ SQL.select(List(log_name, afp_pull_date) ::: table1.columns.tail.map(_.apply(table1))) +
+ table1 + SQL.join_outer + table2 +
+ " ON " + version1(table1) + " = " + version1(table2) +
+ " AND " + version2(table1) + " = " + version2(table2))
- val b_columns = a_columns ::: sessions_table.columns.tail
+ val b_columns = log_name :: pull_date() :: a_columns.tail
val b_table =
SQL.Table("b", b_columns,
- SQL.select(log_name(a_table) :: b_columns.tail) + a_table.query_named +
- SQL.join_inner + table3 + " ON " + log_name(a_table) + " = " + log_name(table3))
+ SQL.select(
+ List(log_name(a_table), pull_date()(table3)) ::: a_columns.tail.map(_.apply(a_table))) +
+ a_table.query_named + SQL.join_outer + table3 +
+ " ON " + version1(a_table) + " = " + version1(table3))
- SQL.Table("isabelle_build_log", b_columns ::: List(ml_statistics),
+ val c_columns = b_columns ::: sessions_table.columns.tail
+ val c_table =
+ SQL.Table("c", c_columns,
+ SQL.select(log_name(b_table) :: c_columns.tail) +
+ b_table.query_named + SQL.join_inner + sessions_table +
+ " ON " + log_name(b_table) + " = " + log_name(sessions_table))
+
+ SQL.Table("isabelle_build_log", c_columns ::: List(ml_statistics),
{
- SQL.select(b_columns.map(_.apply(b_table)) ::: List(ml_statistics)) +
- b_table.query_named + SQL.join_outer + table4 + " ON " +
- log_name(b_table) + " = " + log_name(table4) + " AND " +
- session_name(b_table) + " = " + session_name(table4)
+ SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
+ c_table.query_named + SQL.join_outer + ml_statistics_table +
+ " ON " + log_name(c_table) + " = " + log_name(ml_statistics_table) +
+ " AND " + session_name(c_table) + " = " + session_name(ml_statistics_table)
})
}
}
@@ -905,12 +921,15 @@
}
// pull_date
+ for (afp <- List(false, true))
{
- val table = Data.pull_date_table()
+ val afp_rev = if (afp) Some("") else None
+ val table = Data.pull_date_table(afp)
db2.create_table(table)
db2.using_statement(table.insert())(stmt2 =>
{
- db.using_statement(Data.recent_pull_date_table(days).query)(stmt =>
+ db.using_statement(
+ Data.recent_pull_date_table(days, afp_rev = afp_rev).query)(stmt =>
{
val res = stmt.execute_query()
while (res.next()) {
--- a/src/Pure/Admin/build_status.scala Wed Oct 18 11:53:01 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Wed Oct 18 19:53:19 2017 +0200
@@ -21,7 +21,8 @@
/* data profiles */
- sealed case class Profile(description: String, history: Int, sql: String)
+ sealed case class Profile(
+ description: String, history: Int = 0, afp: Boolean = false, sql: String)
{
def days(options: Options): Int = options.int("build_log_history") max history
@@ -32,7 +33,8 @@
{
Build_Log.Data.universal_table.select(columns, distinct = true,
sql = "WHERE " +
- Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days(options)) + " AND " +
+ Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
+ " AND " +
SQL.member(Build_Log.Data.status.ident,
List(
Build_Log.Session_Status.finished.toString,
@@ -40,7 +42,7 @@
(if (only_sessions.isEmpty) ""
else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
" AND " + SQL.enclose(sql) +
- " ORDER BY " + Build_Log.Data.pull_date)
+ " ORDER BY " + Build_Log.Data.pull_date(afp))
}
}
@@ -109,11 +111,13 @@
def failed: Boolean = status == Build_Log.Session_Status.failed
def present_errors(name: String): XML.Body =
- if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
+ {
+ if (errors.isEmpty) HTML.text(name + print_versions(isabelle_version, afp_version))
else {
HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) ::
- HTML.text(" (" + isabelle_version + ")")
+ HTML.text(print_versions(isabelle_version, afp_version))
}
+ }
}
sealed case class Image(name: String, width: Int, height: Int)
@@ -121,6 +125,14 @@
def path: Path = Path.basic(name)
}
+ def print_versions(isabelle_version: String, afp_version: String): String =
+ {
+ val body =
+ proper_string(isabelle_version).map("Isabelle/" + _).toList :::
+ proper_string(afp_version).map("AFP/" + _).toList
+ if (body.isEmpty) "" else body.mkString(" (", ", ", ")")
+ }
+
def read_data(options: Options,
progress: Progress = No_Progress,
profiles: List[Profile] = default_profiles,
@@ -142,9 +154,10 @@
for (profile <- profiles.sortBy(_.description)) {
progress.echo("input " + quote(profile.description))
+ val afp = profile.afp
val columns =
List(
- Build_Log.Data.pull_date,
+ Build_Log.Data.pull_date(afp),
Build_Log.Prop.build_host,
Build_Log.Prop.isabelle_version,
Build_Log.Prop.afp_version,
@@ -195,18 +208,19 @@
data_stretch += (data_name -> profile.stretch(options))
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
+ val afp_version = res.string(Build_Log.Prop.afp_version)
val ml_stats =
ML_Statistics(
if (ml_statistics)
Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics))
- else Nil, heading = session_name + " (Isabelle/" + isabelle_version + ")")
+ else Nil, heading = session_name + print_versions(isabelle_version, afp_version))
val entry =
Entry(
- pull_date = res.date(Build_Log.Data.pull_date),
+ pull_date = res.date(Build_Log.Data.pull_date(afp)),
isabelle_version = isabelle_version,
- afp_version = res.string(Build_Log.Prop.afp_version),
+ afp_version = afp_version,
timing =
res.timing(
Build_Log.Data.timing_elapsed,
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 18 11:53:01 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 18 19:53:19 2017 +0200
@@ -86,6 +86,7 @@
def recent_items(db: SQL.Database,
days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
{
+ val afp = afp_rev.isDefined
val select =
Build_Log.Data.select_recent_versions(
days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
@@ -95,10 +96,8 @@
{
val known = res.bool(Build_Log.Data.known)
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
- val afp_version =
- if (afp_rev.isEmpty) None
- else proper_string(res.string(Build_Log.Prop.afp_version))
- val pull_date = res.date(Build_Log.Data.pull_date)
+ val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
+ val pull_date = res.date(Build_Log.Data.pull_date(afp))
Item(known, isabelle_version, afp_version, pull_date)
}).toList)
}
@@ -129,7 +128,7 @@
(if (detect == "") "" else " AND " + SQL.enclose(detect))
def profile: Build_Status.Profile =
- Build_Status.Profile(description, history, sql)
+ Build_Status.Profile(description, history = history, afp = afp, sql = sql)
def history_base_filter(hg: Mercurial.Repository): Item => Boolean =
{
--- a/src/Pure/Admin/jenkins.scala Wed Oct 18 11:53:01 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala Wed Oct 18 19:53:19 2017 +0200
@@ -54,11 +54,12 @@
val build_status_profiles: List[Build_Status.Profile] =
build_log_jobs.map(job_name =>
- Build_Status.Profile("jenkins " + job_name, 0,
- Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
- Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
- Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
- " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
+ Build_Status.Profile("jenkins " + job_name,
+ sql =
+ Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
+ Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
+ Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
+ " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
/* job info */