# HG changeset patch
# User wenzelm
# Date 1692970274 -7200
# Node ID a945b541efff1484eb49b29161bd5fbca07496a8
# Parent  2baa77e37406ae53908bb81ac1363aa972c16653
clarified default options: SQLite build_database is unsupported for Isabelle2023, due to lack of proper transaction_lock;

diff -r 2baa77e37406 -r a945b541efff src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Aug 25 11:31:24 2023 +0200
+++ b/src/Pure/Tools/build.scala	Fri Aug 25 15:31:14 2023 +0200
@@ -527,7 +527,9 @@
       var list_builds = false
       var options =
         Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS :::
-          List(Options.Spec.make("build_database")))
+          List(
+            Options.Spec.make("build_database_server"),
+            Options.Spec.make("build_database")))
 
       val getopts = Getopts("""
 Usage: isabelle build_process [OPTIONS]
@@ -618,7 +620,9 @@
       var max_jobs = 1
       var options =
         Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS :::
-          List(Options.Spec.make("build_database")))
+          List(
+            Options.Spec.make("build_database_server"),
+            Options.Spec.make("build_database")))
       var verbose = false
 
       val getopts = Getopts("""
diff -r 2baa77e37406 -r a945b541efff src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Aug 25 11:31:24 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Aug 25 15:31:14 2023 +0200
@@ -838,6 +838,9 @@
   private val _build_database: Option[SQL.Database] =
     try {
       for (db <- store.maybe_open_build_database(server = server)) yield {
+        if (!db.is_postgresql) {
+          error("Required PostgreSQL for cluster build (option database_server)")
+        }
         val store_tables = db.is_postgresql
         Build_Process.private_data.transaction_lock(db,
           create = true,