--- a/src/Pure/Admin/build_log.scala Thu Oct 26 12:36:19 2023 +0200
+++ b/src/Pure/Admin/build_log.scala Thu Oct 26 15:38:27 2023 +0200
@@ -632,7 +632,7 @@
/* SQL data model */
- object Data extends SQL.Data("isabelle_build_log") {
+ object private_data extends SQL.Data("isabelle_build_log") {
override def tables: SQL.Tables =
SQL.Tables(
meta_info_table,
@@ -869,15 +869,15 @@
db.transaction {
db2.transaction {
// main content
- db2.create_table(Data.meta_info_table)
- db2.create_table(Data.sessions_table)
- db2.create_table(Data.theories_table)
- db2.create_table(Data.ml_statistics_table)
+ db2.create_table(private_data.meta_info_table)
+ db2.create_table(private_data.sessions_table)
+ db2.create_table(private_data.theories_table)
+ db2.create_table(private_data.ml_statistics_table)
val recent_log_names =
db.execute_query_statement(
- Data.select_recent_log_names(days),
- List.from[String], res => res.string(Data.log_name))
+ private_data.select_recent_log_names(days),
+ List.from[String], res => res.string(private_data.log_name))
for (log_name <- recent_log_names) {
read_meta_info(db, log_name).foreach(meta_info =>
@@ -894,11 +894,11 @@
// pull_date
for (afp <- List(false, true)) {
val afp_rev = if (afp) Some("") else None
- val table = Data.pull_date_table(afp)
+ val table = private_data.pull_date_table(afp)
db2.create_table(table)
db2.using_statement(table.insert()) { stmt2 =>
db.using_statement(
- Data.recent_pull_date_table(days, afp_rev = afp_rev).query) { stmt =>
+ private_data.recent_pull_date_table(days, afp_rev = afp_rev).query) { stmt =>
using(stmt.execute_query()) { res =>
while (res.next()) {
for ((c, i) <- table.columns.zipWithIndex) {
@@ -912,7 +912,7 @@
}
// full view
- db2.create_view(Data.universal_table)
+ db2.create_view(private_data.universal_table)
}
}
db2.vacuum()
@@ -925,9 +925,9 @@
Set.from[String], res => res.string(column))
def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info): Unit =
- db.using_statement(db.insert_permissive(Data.meta_info_table)) { stmt =>
+ db.using_statement(db.insert_permissive(private_data.meta_info_table)) { stmt =>
stmt.string(1) = log_name
- for ((c, i) <- Data.meta_info_table.columns.tail.zipWithIndex) {
+ for ((c, i) <- private_data.meta_info_table.columns.tail.zipWithIndex) {
if (c.T == SQL.Type.Date) stmt.date(i + 2) = meta_info.get_date(c)
else stmt.string(i + 2) = meta_info.get(c)
}
@@ -935,7 +935,7 @@
}
def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
- db.using_statement(db.insert_permissive(Data.sessions_table)) { stmt =>
+ db.using_statement(db.insert_permissive(private_data.sessions_table)) { stmt =>
val sessions =
if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
else build_info.sessions
@@ -963,7 +963,7 @@
}
def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
- db.using_statement(db.insert_permissive(Data.theories_table)) { stmt =>
+ db.using_statement(db.insert_permissive(private_data.theories_table)) { stmt =>
val sessions =
if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
Build_Info.sessions_dummy
@@ -983,7 +983,7 @@
}
def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info): Unit =
- db.using_statement(db.insert_permissive(Data.ml_statistics_table)) { stmt =>
+ db.using_statement(db.insert_permissive(private_data.ml_statistics_table)) { stmt =>
val ml_stats: List[(String, Option[Bytes])] =
Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
{ case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.compress).proper) },
@@ -1009,7 +1009,7 @@
abstract class Table_Status(table: SQL.Table) {
db.create_table(table)
- private var known: Set[String] = domain(db, table, Data.log_name)
+ private var known: Set[String] = domain(db, table, private_data.log_name)
def required(file: JFile): Boolean = !known(Log_File.plain_name(file))
def required(log_file: Log_File): Boolean = !known(log_file.name)
@@ -1024,19 +1024,19 @@
}
val status =
List(
- new Table_Status(Data.meta_info_table) {
+ new Table_Status(private_data.meta_info_table) {
override def update_db(db: SQL.Database, log_file: Log_File): Unit =
update_meta_info(db, log_file.name, log_file.parse_meta_info())
},
- new Table_Status(Data.sessions_table) {
+ new Table_Status(private_data.sessions_table) {
override def update_db(db: SQL.Database, log_file: Log_File): Unit =
update_sessions(db, log_file.name, log_file.parse_build_info())
},
- new Table_Status(Data.theories_table) {
+ new Table_Status(private_data.theories_table) {
override def update_db(db: SQL.Database, log_file: Log_File): Unit =
update_theories(db, log_file.name, log_file.parse_build_info())
},
- new Table_Status(Data.ml_statistics_table) {
+ new Table_Status(private_data.ml_statistics_table) {
override def update_db(db: SQL.Database, log_file: Log_File): Unit =
if (ml_statistics) {
update_ml_statistics(db, log_file.name,
@@ -1064,18 +1064,18 @@
}
}
- db.create_view(Data.pull_date_table())
- db.create_view(Data.pull_date_table(afp = true))
- db.create_view(Data.universal_table)
+ db.create_view(private_data.pull_date_table())
+ db.create_view(private_data.pull_date_table(afp = true))
+ db.create_view(private_data.universal_table)
errors1
}
def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] = {
- val table = Data.meta_info_table
+ val table = private_data.meta_info_table
val columns = table.columns.tail
db.execute_query_statementO[Meta_Info](
- table.select(columns, sql = Data.log_name.where_equal(log_name)),
+ table.select(columns, sql = private_data.log_name.where_equal(log_name)),
{ res =>
val results =
columns.map(c => c.name ->
@@ -1097,57 +1097,57 @@
session_names: List[String] = Nil,
ml_statistics: Boolean = false
): Build_Info = {
- val table1 = Data.sessions_table
- val table2 = Data.ml_statistics_table
+ val table1 = private_data.sessions_table
+ val table2 = private_data.ml_statistics_table
val columns1 = table1.columns.tail.map(_.apply(table1))
val (columns, from) =
if (ml_statistics) {
- val columns = columns1 ::: List(Data.ml_statistics(table2))
+ val columns = columns1 ::: List(private_data.ml_statistics(table2))
val join =
table1.ident + SQL.join_outer + table2.ident + " ON " +
SQL.and(
- Data.log_name(table1).ident + " = " + Data.log_name(table2).ident,
- Data.session_name(table1).ident + " = " + Data.session_name(table2).ident)
+ private_data.log_name(table1).ident + " = " + private_data.log_name(table2).ident,
+ private_data.session_name(table1).ident + " = " + private_data.session_name(table2).ident)
(columns, SQL.enclose(join))
}
else (columns1, table1.ident)
val where =
SQL.where_and(
- Data.log_name(table1).equal(log_name),
- Data.session_name(table1).ident + " <> ''",
- if_proper(session_names, Data.session_name(table1).member(session_names)))
+ private_data.log_name(table1).equal(log_name),
+ private_data.session_name(table1).ident + " <> ''",
+ if_proper(session_names, private_data.session_name(table1).member(session_names)))
val sessions =
db.execute_query_statement(
SQL.select(columns, sql = from + where),
Map.from[String, Session_Entry],
{ res =>
- val session_name = res.string(Data.session_name)
+ val session_name = res.string(private_data.session_name)
val session_entry =
Session_Entry(
- chapter = res.string(Data.chapter),
- groups = split_lines(res.string(Data.groups)),
- hostname = res.get_string(Data.hostname),
- threads = res.get_int(Data.threads),
+ chapter = res.string(private_data.chapter),
+ groups = split_lines(res.string(private_data.groups)),
+ hostname = res.get_string(private_data.hostname),
+ threads = res.get_int(private_data.threads),
timing =
res.timing(
- Data.timing_elapsed,
- Data.timing_cpu,
- Data.timing_gc),
+ private_data.timing_elapsed,
+ private_data.timing_cpu,
+ private_data.timing_gc),
ml_timing =
res.timing(
- Data.ml_timing_elapsed,
- Data.ml_timing_cpu,
- Data.ml_timing_gc),
- sources = res.get_string(Data.sources),
- heap_size = res.get_long(Data.heap_size).map(Space.bytes),
- status = res.get_string(Data.status).map(Session_Status.valueOf),
- errors = uncompress_errors(res.bytes(Data.errors), cache = cache),
+ private_data.ml_timing_elapsed,
+ private_data.ml_timing_cpu,
+ private_data.ml_timing_gc),
+ sources = res.get_string(private_data.sources),
+ heap_size = res.get_long(private_data.heap_size).map(Space.bytes),
+ status = res.get_string(private_data.status).map(Session_Status.valueOf),
+ errors = uncompress_errors(res.bytes(private_data.errors), cache = cache),
ml_statistics =
if (ml_statistics) {
- Properties.uncompress(res.bytes(Data.ml_statistics), cache = cache)
+ Properties.uncompress(res.bytes(private_data.ml_statistics), cache = cache)
}
else Nil)
session_name -> session_entry
--- a/src/Pure/Admin/build_status.scala Thu Oct 26 12:36:19 2023 +0200
+++ b/src/Pure/Admin/build_status.scala Thu Oct 26 15:38:27 2023 +0200
@@ -38,36 +38,36 @@
): PostgreSQL.Source = {
val columns =
List(
- Build_Log.Data.pull_date(afp = false),
- Build_Log.Data.pull_date(afp = true),
+ Build_Log.private_data.pull_date(afp = false),
+ Build_Log.private_data.pull_date(afp = true),
Build_Log.Prop.build_host,
Build_Log.Prop.isabelle_version,
Build_Log.Prop.afp_version,
Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
Build_Log.Settings.ML_PLATFORM,
- Build_Log.Data.session_name,
- Build_Log.Data.chapter,
- Build_Log.Data.groups,
- 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,
- Build_Log.Data.heap_size,
- Build_Log.Data.status,
- Build_Log.Data.errors) :::
- (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil)
+ Build_Log.private_data.session_name,
+ Build_Log.private_data.chapter,
+ Build_Log.private_data.groups,
+ Build_Log.private_data.threads,
+ Build_Log.private_data.timing_elapsed,
+ Build_Log.private_data.timing_cpu,
+ Build_Log.private_data.timing_gc,
+ Build_Log.private_data.ml_timing_elapsed,
+ Build_Log.private_data.ml_timing_cpu,
+ Build_Log.private_data.ml_timing_gc,
+ Build_Log.private_data.heap_size,
+ Build_Log.private_data.status,
+ Build_Log.private_data.errors) :::
+ (if (ml_statistics) List(Build_Log.private_data.ml_statistics) else Nil)
- Build_Log.Data.universal_table.select(columns, distinct = true, sql =
+ Build_Log.private_data.universal_table.select(columns, distinct = true, sql =
SQL.where_and(
- Build_Log.Data.pull_date(afp).ident + " > " + Build_Log.Data.recent_time(days(options)),
- Build_Log.Data.status.member(
+ Build_Log.private_data.pull_date(afp).ident + " > " + Build_Log.private_data.recent_time(days(options)),
+ Build_Log.private_data.status.member(
List(
Build_Log.Session_Status.finished.toString,
Build_Log.Session_Status.failed.toString)),
- if_proper(only_sessions, Build_Log.Data.session_name.member(only_sessions)),
+ if_proper(only_sessions, Build_Log.private_data.session_name.member(only_sessions)),
if_proper(sql, SQL.enclose(sql))))
}
}
@@ -261,16 +261,16 @@
db.using_statement(sql) { stmt =>
using(stmt.execute_query()) { res =>
while (res.next()) {
- val session_name = res.string(Build_Log.Data.session_name)
- val chapter = res.string(Build_Log.Data.chapter)
- val groups = split_lines(res.string(Build_Log.Data.groups))
+ val session_name = res.string(Build_Log.private_data.session_name)
+ val chapter = res.string(Build_Log.private_data.chapter)
+ val groups = split_lines(res.string(Build_Log.private_data.groups))
val threads = {
val threads1 =
res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
case Threads_Option(Value.Int(i)) => i
case _ => 1
}
- val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
+ val threads2 = res.get_int(Build_Log.private_data.threads).getOrElse(1)
threads1 max threads2
}
val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
@@ -292,7 +292,7 @@
val ml_stats =
ML_Statistics(
if (ml_statistics) {
- Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache)
+ Properties.uncompress(res.bytes(Build_Log.private_data.ml_statistics), cache = store.cache)
}
else Nil,
domain = ml_statistics_domain,
@@ -301,32 +301,32 @@
val entry =
Entry(
chapter = chapter,
- pull_date = res.date(Build_Log.Data.pull_date(afp = false)),
+ pull_date = res.date(Build_Log.private_data.pull_date(afp = false)),
afp_pull_date =
- if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None,
+ if (afp) res.get_date(Build_Log.private_data.pull_date(afp = true)) else None,
isabelle_version = isabelle_version,
afp_version = afp_version,
timing =
res.timing(
- Build_Log.Data.timing_elapsed,
- Build_Log.Data.timing_cpu,
- Build_Log.Data.timing_gc),
+ Build_Log.private_data.timing_elapsed,
+ Build_Log.private_data.timing_cpu,
+ Build_Log.private_data.timing_gc),
ml_timing =
res.timing(
- Build_Log.Data.ml_timing_elapsed,
- Build_Log.Data.ml_timing_cpu,
- Build_Log.Data.ml_timing_gc),
+ Build_Log.private_data.ml_timing_elapsed,
+ Build_Log.private_data.ml_timing_cpu,
+ Build_Log.private_data.ml_timing_gc),
maximum_code = Space.B(ml_stats.maximum(ML_Statistics.CODE_SIZE)),
average_code = Space.B(ml_stats.average(ML_Statistics.CODE_SIZE)),
maximum_stack = Space.B(ml_stats.maximum(ML_Statistics.STACK_SIZE)),
average_stack = Space.B(ml_stats.average(ML_Statistics.STACK_SIZE)),
maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)),
average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)),
- stored_heap = Space.bytes(res.long(Build_Log.Data.heap_size)),
- status = Build_Log.Session_Status.valueOf(res.string(Build_Log.Data.status)),
+ stored_heap = Space.bytes(res.long(Build_Log.private_data.heap_size)),
+ status = Build_Log.Session_Status.valueOf(res.string(Build_Log.private_data.status)),
errors =
Build_Log.uncompress_errors(
- res.bytes(Build_Log.Data.errors), cache = store.cache))
+ res.bytes(Build_Log.private_data.errors), cache = store.cache))
val sessions = data_entries.getOrElse(data_name, Map.empty)
val session =
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Oct 26 12:36:19 2023 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Oct 26 15:38:27 2023 +0200
@@ -118,14 +118,14 @@
val afp = afp_rev.isDefined
db.execute_query_statement(
- Build_Log.Data.select_recent_versions(
+ Build_Log.private_data.select_recent_versions(
days = days, rev = rev, afp_rev = afp_rev, sql = SQL.where(sql)),
List.from[Item],
{ res =>
- val known = res.bool(Build_Log.Data.known)
+ val known = res.bool(Build_Log.private_data.known)
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
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))
+ val pull_date = res.date(Build_Log.private_data.pull_date(afp))
Item(known, isabelle_version, afp_version, pull_date)
})
}
--- a/src/Pure/Tools/build_schedule.scala Thu Oct 26 12:36:19 2023 +0200
+++ b/src/Pure/Tools/build_schedule.scala Thu Oct 26 15:38:27 2023 +0200
@@ -408,7 +408,7 @@
private final lazy val _log_database: SQL.Database =
try {
val db = _log_store.open_database(server = this.server)
- Build_Log.Data.tables.foreach(db.create_table(_))
+ Build_Log.private_data.tables.foreach(db.create_table(_))
db
}
catch { case exn: Throwable => close(); throw exn }
@@ -447,8 +447,8 @@
val build_history =
for {
log_name <- _log_database.execute_query_statement(
- Build_Log.Data.meta_info_table.select(List(Build_Log.Data.log_name)),
- List.from[String], res => res.string(Build_Log.Data.log_name))
+ Build_Log.private_data.meta_info_table.select(List(Build_Log.private_data.log_name)),
+ List.from[String], res => res.string(Build_Log.private_data.log_name))
meta_info <- _log_store.read_meta_info(_log_database, log_name)
build_info = _log_store.read_build_info(_log_database, log_name)
} yield (meta_info, build_info)