more robust database setup;
authorwenzelm
Fri, 30 Jun 2023 16:26:03 +0200
changeset 78234 13863eaf372a
parent 78233 1a12e6246212
child 78235 aece9a063271
more robust database setup;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Jun 30 16:04:53 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jun 30 16:26:03 2023 +0200
@@ -80,15 +80,6 @@
           }
       }
 
-    using_option(store.maybe_open_build_database()) { db =>
-      val shared_db = db.is_postgresql
-      Data.transaction_lock(db, create = true) {
-        Data.clean_build(db)
-        if (shared_db) Store.Data.tables.lock(db, create = true)
-      }
-      Data.vacuum(db, more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty)
-    }
-
     val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
 
     new Context(store, build_deps, sessions, ordering, ml_platform, hostname, numa_nodes,
@@ -826,7 +817,18 @@
     catch { case exn: Throwable => close(); throw exn }
 
   private val _build_database: Option[SQL.Database] =
-    try { store.maybe_open_build_database() }
+    try {
+      for (db <- store.maybe_open_build_database()) yield {
+        val shared_db = db.is_postgresql
+        Build_Process.Data.transaction_lock(db, create = true) {
+          Build_Process.Data.clean_build(db)
+          if (shared_db) Store.Data.tables.lock(db, create = true)
+        }
+        Build_Process.Data.vacuum(db,
+          more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty)
+        db
+      }
+    }
     catch { case exn: Throwable => close(); throw exn }
 
   private val _host_database: Option[SQL.Database] =