--- 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"
--- 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,
--- 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 }
}
--- 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