more robust init_database();
proper treatment of views, not tables (amending dd350a41594c);
--- a/src/Pure/Admin/build_log.scala Thu Oct 26 16:04:48 2023 +0200
+++ b/src/Pure/Admin/build_log.scala Thu Oct 26 22:10:22 2023 +0200
@@ -639,10 +639,7 @@
sessions_table,
theories_table,
ml_statistics_table,
- isabelle_afp_versions_table,
- universal_table,
- pull_date_table(afp = true),
- pull_date_table())
+ isabelle_afp_versions_table)
/* main content */
@@ -856,6 +853,15 @@
ssh_user = options.string("build_log_ssh_user"),
synchronous_commit = options.string("build_log_database_synchronous_commit"))
+ def init_database(db: SQL.Database, minimal: Boolean = false): Unit =
+ private_data.transaction_lock(db, create = true, label = "build_log_init") {
+ if (!minimal) {
+ 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)
+ }
+
def snapshot_database(
db: PostgreSQL.Database,
sqlite_database: Path,
@@ -1003,6 +1009,8 @@
progress: Progress = new Progress,
errors: Multi_Map[String, String] = Multi_Map.empty
): Multi_Map[String, String] = {
+ init_database(db)
+
var errors1 = errors
def add_error(name: String, exn: Throwable): Unit = {
errors1 = errors1.insert(name, Exn.print(exn))
@@ -1053,7 +1061,7 @@
val log_files =
Par_List.map[JFile, Exn.Result[Log_File]](
file => Exn.result { Log_File(file) }, file_group)
- private_data.transaction_lock(db, create = true, label = "build_log_database") {
+ private_data.transaction_lock(db, label = "build_log_database") {
for (case Exn.Res(log_file) <- log_files) {
progress.echo("Log " + quote(log_file.name), verbose = true)
try { status.foreach(_.update(log_file)) }
@@ -1065,10 +1073,6 @@
}
}
- 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
}
--- a/src/Pure/Tools/build_schedule.scala Thu Oct 26 16:04:48 2023 +0200
+++ b/src/Pure/Tools/build_schedule.scala Thu Oct 26 22:10:22 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.private_data.tables.foreach(db.create_table(_))
+ _log_store.init_database(db)
db
}
catch { case exn: Throwable => close(); throw exn }