# HG changeset patch
# User wenzelm
# Date 1689714219 -7200
# Node ID 63d55ba90a9f541444845fac2b839640ed3bcc13
# Parent  facf1a324807712e6f55e08a5a25cb2d5241e640
more options for performance tuning;

diff -r facf1a324807 -r 63d55ba90a9f etc/options
--- a/etc/options	Tue Jul 18 21:06:11 2023 +0200
+++ b/etc/options	Tue Jul 18 23:03:39 2023 +0200
@@ -390,6 +390,8 @@
 option build_database_ssh_host : string = "" for connection
 option build_database_ssh_user : string = "" for connection
 option build_database_ssh_port : int = 0 for connection
+option build_database_synchronous_commit : string = "off" for connection
+  -- "see https://www.postgresql.org/docs/current/runtime-config-wal.html#GUC-SYNCHRONOUS-COMMIT"
 
 
 section "Build Log Database"
@@ -404,6 +406,8 @@
 option build_log_ssh_port : int = 0 for connection
 option build_log_history : int = 30  -- "length of relevant history (in days)"
 option build_log_transaction_size : int = 1  -- "number of log files for each db update"
+option build_log_database_synchronous_commit : string = "off" for connection
+  -- "see https://www.postgresql.org/docs/current/runtime-config-wal.html#GUC-SYNCHRONOUS-COMMIT"
 
 
 section "Isabelle/Scala/ML system channel"
diff -r facf1a324807 -r 63d55ba90a9f src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Jul 18 21:06:11 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Jul 18 23:03:39 2023 +0200
@@ -841,7 +841,8 @@
         port = options.int("build_log_database_port"),
         ssh_host = options.string("build_log_ssh_host"),
         ssh_port = options.int("build_log_ssh_port"),
-        ssh_user = options.string("build_log_ssh_user"))
+        ssh_user = options.string("build_log_ssh_user"),
+        synchronous_commit = options.string("build_log_database_synchronous_commit"))
 
     def snapshot_database(
       db: PostgreSQL.Database,
diff -r facf1a324807 -r 63d55ba90a9f src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Jul 18 21:06:11 2023 +0200
+++ b/src/Pure/General/sql.scala	Tue Jul 18 23:03:39 2023 +0200
@@ -636,6 +636,7 @@
     database: String = "",
     server: SSH.Server = default_server,
     server_close: Boolean = false,
+    synchronous_commit: String = "off"
   ): Database = {
     init_jdbc
 
@@ -649,7 +650,14 @@
     val print = user + "@" + server + "/" + name + if_proper(ssh, " via ssh " + ssh.get)
 
     val connection = DriverManager.getConnection(url, user, password)
-    new Database(connection, print, server, server_close)
+    val db = new Database(connection, print, server, server_close)
+
+    try {
+      db.execute_statement("SET synchronous_commit = " + SQL.string(synchronous_commit))
+    }
+    catch { case exn: Throwable => db.close(); throw exn }
+
+    db
   }
 
   def open_server(
@@ -680,7 +688,8 @@
     port: Int = 0,
     ssh_host: String = "",
     ssh_port: Int = 0,
-    ssh_user: String = ""
+    ssh_user: String = "",
+    synchronous_commit: String = "off"
   ): PostgreSQL.Database = {
     val db_server =
       if (server.defined) server
@@ -691,7 +700,7 @@
     val server_close = !server.defined
     try {
       open_database(user = user, password = password, database = database,
-        server = db_server, server_close = server_close)
+        server = db_server, server_close = server_close, synchronous_commit = synchronous_commit)
     }
     catch { case exn: Throwable if server_close => db_server.close(); throw exn }
   }
diff -r facf1a324807 -r 63d55ba90a9f src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Tue Jul 18 21:06:11 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jul 18 23:03:39 2023 +0200
@@ -306,7 +306,8 @@
       port = options.int("build_database_port"),
       ssh_host = options.string("build_database_ssh_host"),
       ssh_port = options.int("build_database_ssh_port"),
-      ssh_user = options.string("build_database_ssh_user"))
+      ssh_user = options.string("build_database_ssh_user"),
+      synchronous_commit = options.string("build_database_synchronous_commit"))
 
   def maybe_open_database_server(server: SSH.Server = SSH.no_server): Option[SQL.Database] =
     if (build_database_server) Some(open_database_server(server = server)) else None