clarified default options: SQLite build_database is unsupported for Isabelle2023, due to lack of proper transaction_lock;
authorwenzelm
Fri, 25 Aug 2023 15:31:14 +0200
changeset 78577 a945b541efff
parent 78576 2baa77e37406
child 78578 5ccf921a2c3d
clarified default options: SQLite build_database is unsupported for Isabelle2023, due to lack of proper transaction_lock;
src/Pure/Tools/build.scala
src/Pure/Tools/build_process.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("""
--- 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,