--- a/src/Pure/Admin/build_log.scala Mon May 08 21:58:15 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Mon May 08 22:21:36 2017 +0200
@@ -658,6 +658,7 @@
val heap_size = SQL.Column.long("heap_size")
val status = SQL.Column.string("status")
val ml_statistics = SQL.Column.bytes("ml_statistics")
+ val known = SQL.Column.bool("known")
val meta_info_table =
build_log_table("meta_info", log_name :: Prop.all_props ::: Settings.all_settings)
@@ -689,11 +690,13 @@
def recent_time(days: Int): SQL.Source =
"now() - INTERVAL '" + days.max(0) + " days'"
- def recent_pull_date_table(days: Int): SQL.Table =
+ def recent_pull_date_table(days: Int, rev: String = ""): SQL.Table =
{
val table = pull_date_table
SQL.Table("recent_pull_date", table.columns,
- table.select(table.columns, "WHERE " + pull_date(table) + " > " + recent_time(days)))
+ table.select(table.columns,
+ "WHERE " + pull_date(table) + " > " + recent_time(days) +
+ (if (rev == "") "" else " OR " + Prop.isabelle_version(table) + " = " + SQL.string(rev))))
}
def select_recent_log_names(days: Int): SQL.Source =
@@ -704,6 +707,22 @@
" ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
}
+ def select_recent_isabelle_versions(days: Int, rev: String = "", sql: SQL.Source = "")
+ : SQL.Source =
+ {
+ val table1 = recent_pull_date_table(days, rev = rev)
+ val table2 = meta_info_table
+ val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql))
+
+ val columns =
+ List(Prop.isabelle_version(table1), pull_date(table1),
+ known.copy(expr = log_name(aux_table) + " IS NOT NULL"))
+ SQL.select(columns, distinct = true) +
+ table1.query_named + SQL.join_outer + aux_table.query_named +
+ " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(aux_table) +
+ " ORDER BY " + pull_date(table1) + " DESC"
+ }
+
/* universal view on main data */
--- a/src/Pure/Admin/isabelle_cronjob.scala Mon May 08 21:58:15 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Mon May 08 22:21:36 2017 +0200
@@ -73,6 +73,11 @@
/* remote build_history */
+ sealed case class Item(known: Boolean, isabelle_version: String, pull_date: Date)
+ {
+ def unknown: Boolean = !known
+ }
+
sealed case class Remote_Build(
description: String,
host: String,
@@ -83,13 +88,47 @@
args: String = "",
detect: SQL.Source = "")
{
+ def sql: SQL.Source =
+ 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))
+
def profile: Build_Status.Profile =
+ Build_Status.Profile(description, sql)
+
+ def pick(options: Options, rev: String = ""): Option[String] =
{
- 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(description, sql)
+ val store = Build_Log.store(options)
+ using(store.open_database())(db =>
+ {
+ val select =
+ Build_Log.Data.select_recent_isabelle_versions(
+ days = options.int("build_log_history"), rev = rev, sql = "WHERE " + sql)
+
+ val recent_items =
+ db.using_statement(select)(stmt =>
+ stmt.execute_query().iterator(res =>
+ {
+ val known = res.bool(Build_Log.Data.known)
+ val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
+ val pull_date = res.date(Build_Log.Data.pull_date)
+ Item(known, isabelle_version, pull_date)
+ }).toList)
+
+ def unknown_runs(items: List[Item]): List[List[Item]] =
+ {
+ val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
+ if (run.nonEmpty) run :: unknown_runs(rest) else Nil
+ }
+
+ if (rev == "" || recent_items.exists(item => item.known && item.isabelle_version == rev)) {
+ unknown_runs(recent_items).sortBy(_.length).reverse match {
+ case longest_run :: _ => Some(longest_run(longest_run.length / 2).isabelle_version)
+ case _ => None
+ }
+ }
+ else Some(rev)
+ })
}
}
@@ -306,10 +345,11 @@
val rev = Mercurial.repository(isabelle_repos).id()
run(main_start_date,
- Logger_Task("isabelle_cronjob", _ =>
+ Logger_Task("isabelle_cronjob", logger =>
run_now(
SEQ(List(build_release, build_history_base,
- PAR(remote_builds.map(seq => SEQ(seq.map(remote_build_history(rev, _))))),
+ PAR(remote_builds.map(seq =>
+ SEQ(seq.flatMap(r => r.pick(logger.options, rev).map(remote_build_history(_, r)))))),
Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
Logger_Task("build_log_database",
logger => Isabelle_Devel.build_log_database(logger.options)),