more robust init_database();
authorwenzelm
Thu, 26 Oct 2023 22:10:22 +0200
changeset 78851 db37cae970a6
parent 78850 3069da1743bc
child 78852 2700e4b484f7
more robust init_database(); proper treatment of views, not tables (amending dd350a41594c);
src/Pure/Admin/build_log.scala
src/Pure/Tools/build_schedule.scala
--- 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 }