# HG changeset patch # User wenzelm # Date 1688135163 -7200 # Node ID 13863eaf372a4ce9996bd0fd8f7a34e423bbf8f3 # Parent 1a12e6246212846acd310f7c0284a6abc37f4a38 more robust database setup; diff -r 1a12e6246212 -r 13863eaf372a 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] =