diff -r 593053cac3be -r 486f4af28db9 src/Pure/Admin/build_log.scala --- 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()) {