--- a/src/Pure/Admin/build_log.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/Admin/build_log.scala Sat Jul 08 16:48:15 2023 +0200
@@ -658,21 +658,23 @@
val known = SQL.Column.bool("known")
val meta_info_table =
- make_table("meta_info", log_name :: Prop.all_props ::: Settings.all_settings)
+ make_table(log_name :: Prop.all_props ::: Settings.all_settings, name = "meta_info")
val sessions_table =
- make_table("sessions",
+ make_table(
List(log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu,
timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
- heap_size, status, errors, sources))
+ heap_size, status, errors, sources),
+ name = "sessions")
val theories_table =
- make_table("theories",
+ make_table(
List(log_name, session_name, theory_name, theory_timing_elapsed, theory_timing_cpu,
- theory_timing_gc))
+ theory_timing_gc),
+ name = "theories")
val ml_statistics_table =
- make_table("ml_statistics", List(log_name, session_name, ml_statistics))
+ make_table(List(log_name, session_name, ml_statistics), name = "ml_statistics")
/* AFP versions */
@@ -680,9 +682,11 @@
val isabelle_afp_versions_table: SQL.Table = {
val version1 = Prop.isabelle_version
val version2 = Prop.afp_version
- make_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
- SQL.select(List(version1, version2), distinct = true) + meta_info_table +
- SQL.where_and(version1.defined, version2.defined))
+ make_table(List(version1.make_primary_key, version2),
+ body =
+ SQL.select(List(version1, version2), distinct = true) + meta_info_table +
+ SQL.where_and(version1.defined, version2.defined),
+ name = "isabelle_afp_versions")
}
@@ -697,12 +701,14 @@
if (afp) ("afp_pull_date", List(Prop.isabelle_version, Prop.afp_version))
else ("pull_date", List(Prop.isabelle_version))
- make_table(name, versions.map(_.make_primary_key) ::: List(pull_date(afp)),
- "SELECT " + versions.mkString(", ") +
- ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
- " FROM " + meta_info_table +
- " WHERE " + SQL.AND((versions ::: List(Prop.build_start)).map(_.defined)) +
- " GROUP BY " + versions.mkString(", "))
+ make_table(versions.map(_.make_primary_key) ::: List(pull_date(afp)),
+ body =
+ "SELECT " + versions.mkString(", ") +
+ ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
+ " FROM " + meta_info_table +
+ " WHERE " + SQL.AND((versions ::: List(Prop.build_start)).map(_.defined)) +
+ " GROUP BY " + versions.mkString(", "),
+ name = name)
}
@@ -794,14 +800,13 @@
b_table.query_named + SQL.join_inner + sessions_table +
" ON " + log_name(b_table) + " = " + log_name(sessions_table))
- make_table("", c_columns ::: List(ml_statistics),
- {
+ make_table(c_columns ::: List(ml_statistics),
+ body =
SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
c_table.query_named + SQL.join_outer + ml_statistics_table + " ON " +
SQL.and(
log_name(c_table).ident + " = " + log_name(ml_statistics_table).ident,
- session_name(c_table).ident + " = " + session_name(ml_statistics_table).ident)
- })
+ session_name(c_table).ident + " = " + session_name(ml_statistics_table).ident))
}
}
--- a/src/Pure/General/sql.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/General/sql.scala Sat Jul 08 16:48:15 2023 +0200
@@ -252,18 +252,14 @@
def transaction_lock[A](
db: Database,
- more_tables: Tables = Tables.empty,
create: Boolean = false,
synchronized: Boolean = false,
)(body: => A): A = {
- def run: A = db.transaction { (tables ::: more_tables).lock(db, create = create); body }
+ def run: A = db.transaction { tables.lock(db, create = create); body }
if (synchronized) db.synchronized { run } else run
}
- def vacuum(db: Database, more_tables: Tables = Tables.empty): Unit =
- db.vacuum(tables = tables ::: more_tables)
-
- def make_table(name: String, columns: List[Column], body: String = ""): Table = {
+ def make_table(columns: List[Column], body: String = "", name: String = ""): Table = {
val table_name =
List(proper_string(table_prefix), proper_string(name)).flatten.mkString("_")
require(table_name.nonEmpty, "Undefined database table name")
--- a/src/Pure/ML/ml_heap.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/ML/ml_heap.scala Sat Jul 08 16:48:15 2023 +0200
@@ -55,7 +55,7 @@
val size = SQL.Column.long("size")
val digest = SQL.Column.string("digest")
- val table = make_table("", List(name, size, digest))
+ val table = make_table(List(name, size, digest))
}
object Slices {
@@ -63,7 +63,7 @@
val slice = SQL.Column.int("slice").make_primary_key
val content = SQL.Column.bytes("content")
- val table = make_table("slices", List(name, slice, content))
+ val table = make_table(List(name, slice, content), name = "slices")
}
def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =
--- a/src/Pure/System/host.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/System/host.scala Sat Jul 08 16:48:15 2023 +0200
@@ -104,7 +104,7 @@
val hostname = SQL.Column.string("hostname").make_primary_key
val numa_next = SQL.Column.int("numa_next")
- val table = make_table("node_info", List(hostname, numa_next))
+ val table = make_table(List(hostname, numa_next), name = "node_info")
}
def read_numa_next(db: SQL.Database, hostname: String): Int =
--- a/src/Pure/System/progress.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/System/progress.scala Sat Jul 08 16:48:15 2023 +0200
@@ -51,7 +51,7 @@
val context = SQL.Column.long("context").make_primary_key
val stopped = SQL.Column.bool("stopped")
- val table = make_table("", List(context_uuid, context, stopped))
+ val table = make_table(List(context_uuid, context, stopped))
}
object Agents {
@@ -66,8 +66,10 @@
val stop = SQL.Column.date("stop")
val seen = SQL.Column.long("seen")
- val table = make_table("agents",
- List(agent_uuid, context_uuid, kind, hostname, java_pid, java_start, start, stamp, stop, seen))
+ val table =
+ make_table(
+ List(agent_uuid, context_uuid, kind, hostname, java_pid, java_start, start, stamp, stop, seen),
+ name = "agents")
}
object Messages {
@@ -80,7 +82,7 @@
val text = SQL.Column.string("text")
val verbose = SQL.Column.bool("verbose")
- val table = make_table("messages", List(context, serial, kind, text, verbose))
+ val table = make_table(List(context, serial, kind, text, verbose), name = "messages")
}
def read_progress_context(db: SQL.Database, context_uuid: String): Option[Long] =
@@ -289,7 +291,7 @@
stmt.long(10) = 0L
})
}
- if (context_uuid == _agent_uuid) Progress.Data.vacuum(db)
+ if (context_uuid == _agent_uuid) db.vacuum(Progress.Data.tables)
}
def exit(close: Boolean = false): Unit = synchronized {
--- a/src/Pure/Thy/document_build.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/Thy/document_build.scala Sat Jul 08 16:48:15 2023 +0200
@@ -54,58 +54,63 @@
/* SQL data model */
- object Data {
- val session_name = SQL.Column.string("session_name").make_primary_key
- val name = SQL.Column.string("name").make_primary_key
- val sources = SQL.Column.string("sources")
- val log_xz = SQL.Column.bytes("log_xz")
- val pdf = SQL.Column.bytes("pdf")
+ object Data extends SQL.Data("isabelle_documents") {
+ override lazy val tables = SQL.Tables(Base.table)
- val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
+ object Base {
+ val session_name = SQL.Column.string("session_name").make_primary_key
+ val name = SQL.Column.string("name").make_primary_key
+ val sources = SQL.Column.string("sources")
+ val log_xz = SQL.Column.bytes("log_xz")
+ val pdf = SQL.Column.bytes("pdf")
+
+ val table = make_table(List(session_name, name, sources, log_xz, pdf))
+ }
def where_equal(session_name: String, name: String = ""): SQL.Source =
SQL.where_and(
- Data.session_name.equal(session_name),
- if_proper(name, Data.name.equal(name)))
+ Base.session_name.equal(session_name),
+ if_proper(name, Base.name.equal(name)))
+
+ def clean_session(db: SQL.Database, session_name: String): Unit =
+ db.execute_statement(Base.table.delete(sql = Base.session_name.where_equal(session_name)))
+
+ def read_document(
+ db: SQL.Database,
+ session_name: String,
+ name: String
+ ): Option[Document_Output] = {
+ db.execute_query_statementO[Document_Output](
+ Base.table.select(sql = where_equal(session_name, name = name)),
+ { res =>
+ val name = res.string(Base.name)
+ val sources = res.string(Base.sources)
+ val log_xz = res.bytes(Base.log_xz)
+ val pdf = res.bytes(Base.pdf)
+ Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf)
+ }
+ )
+ }
+
+ def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
+ db.execute_statement(Base.table.insert(), body =
+ { stmt =>
+ stmt.string(1) = session_name
+ stmt.string(2) = doc.name
+ stmt.string(3) = doc.sources.toString
+ stmt.bytes(4) = doc.log_xz
+ stmt.bytes(5) = doc.pdf
+ })
}
- def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
- db.execute_query_statement(
- Data.table.select(List(Data.name, Data.sources), sql = Data.where_equal(session_name)),
- List.from[Document_Input],
- { res =>
- val name = res.string(Data.name)
- val sources = res.string(Data.sources)
- Document_Input(name, SHA1.fake_shasum(sources))
- }
- )
+ def clean_session(db: SQL.Database, session_name: String): Unit =
+ Data.transaction_lock(db, create = true) { Data.clean_session(db, session_name) }
- def read_document(
- db: SQL.Database,
- session_name: String,
- name: String
- ): Option[Document_Output] = {
- db.execute_query_statementO[Document_Output](
- Data.table.select(sql = Data.where_equal(session_name, name)),
- { res =>
- val name = res.string(Data.name)
- val sources = res.string(Data.sources)
- val log_xz = res.bytes(Data.log_xz)
- val pdf = res.bytes(Data.pdf)
- Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf)
- }
- )
- }
+ def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
+ Data.transaction_lock(db) { Data.read_document(db, session_name, name) }
def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
- db.execute_statement(Data.table.insert(), body =
- { stmt =>
- stmt.string(1) = session_name
- stmt.string(2) = doc.name
- stmt.string(3) = doc.sources.toString
- stmt.bytes(4) = doc.log_xz
- stmt.bytes(5) = doc.pdf
- })
+ Data.transaction_lock(db) { Data.write_document(db, session_name, doc) }
/* background context */
--- a/src/Pure/Thy/export.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/Thy/export.scala Sat Jul 08 16:48:15 2023 +0200
@@ -51,6 +51,9 @@
if_proper(theory_name, Base.theory_name.equal(theory_name)),
if_proper(name, Base.name.equal(name)))
+ def clean_session(db: SQL.Database, session_name: String): Unit =
+ db.execute_statement(Base.table.delete(sql = where_equal(session_name)))
+
def readable_entry(db: SQL.Database, entry_name: Entry_Name): Boolean = {
db.execute_query_statementB(
Base.table.select(List(Base.name),
@@ -200,6 +203,9 @@
(entry_name: Entry_Name) => regs.exists(_.matches(entry_name.compound_name))
}
+ def clean_session(db: SQL.Database, session_name: String): Unit =
+ Data.transaction_lock(db, create = true) { Data.clean_session(db, session_name) }
+
def read_theory_names(db: SQL.Database, session_name: String): List[String] =
Data.transaction_lock(db) { Data.read_theory_names(db, session_name) }
--- a/src/Pure/Thy/store.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/Thy/store.scala Sat Jul 08 16:48:15 2023 +0200
@@ -78,9 +78,7 @@
/* SQL data model */
object Data extends SQL.Data() {
- override lazy val tables =
- SQL.Tables(Session_Info.table, Sources.table,
- Export.Data.Base.table, Document_Build.Data.table)
+ override lazy val tables = SQL.Tables(Session_Info.table, Sources.table)
object Session_Info {
val session_name = SQL.Column.string("session_name").make_primary_key
@@ -127,6 +125,54 @@
if_proper(name, Sources.name.equal(name)))
}
+ def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
+ db.execute_query_statementO[Bytes](
+ Session_Info.table.select(List(column), sql = Session_Info.session_name.where_equal(name)),
+ res => res.bytes(column)
+ ).getOrElse(Bytes.empty)
+
+ def read_properties(
+ db: SQL.Database, name: String, column: SQL.Column, cache: Term.Cache
+ ): List[Properties.T] = Properties.uncompress(read_bytes(db, name, column), cache = cache)
+
+ def read_session_timing(db: SQL.Database, name: String, cache: Term.Cache): Properties.T =
+ Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache)
+
+ def read_command_timings(db: SQL.Database, name: String): Bytes =
+ read_bytes(db, name, Session_Info.command_timings)
+
+ def read_theory_timings(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] =
+ read_properties(db, name, Session_Info.theory_timings, cache)
+
+ def read_ml_statistics(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] =
+ read_properties(db, name, Session_Info.ml_statistics, cache)
+
+ def read_task_statistics(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] =
+ read_properties(db, name, Session_Info.task_statistics, cache)
+
+ def read_errors(db: SQL.Database, name: String, cache: Term.Cache): List[String] =
+ Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
+
+ def read_build(db: SQL.Database, name: String): Option[Store.Build_Info] = {
+ if (db.tables.contains(Session_Info.table.name)) {
+ db.execute_query_statementO[Store.Build_Info](
+ Session_Info.table.select(sql = Session_Info.session_name.where_equal(name)),
+ { res =>
+ val uuid =
+ try { Option(res.string(Session_Info.uuid)).getOrElse("") }
+ catch { case _: SQLException => "" }
+ Store.Build_Info(
+ SHA1.fake_shasum(res.string(Session_Info.sources)),
+ SHA1.fake_shasum(res.string(Session_Info.input_heaps)),
+ SHA1.fake_shasum(res.string(Session_Info.output_heap)),
+ res.int(Session_Info.return_code),
+ uuid)
+ }
+ )
+ }
+ else None
+ }
+
def write_session_info(
db: SQL.Database,
cache: Compress.Cache,
@@ -134,7 +180,7 @@
build_log: Build_Log.Session_Info,
build: Build_Info
): Unit = {
- db.execute_statement(Store.Data.Session_Info.table.insert(), body =
+ db.execute_statement(Session_Info.table.insert(), body =
{ stmt =>
stmt.string(1) = session_name
stmt.bytes(2) = Properties.encode(build_log.session_timing)
@@ -165,9 +211,9 @@
def read_sources(
db: SQL.Database,
- cache: Compress.Cache,
session_name: String,
- name: String = ""
+ name: String,
+ cache: Compress.Cache
): List[Source_File] = {
db.execute_query_statement(
Sources.table.select(
@@ -361,19 +407,6 @@
}
- /* SQL database content */
-
- def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes =
- db.execute_query_statementO[Bytes](
- Store.Data.Session_Info.table.select(List(column),
- sql = Store.Data.Session_Info.session_name.where_equal(name)),
- res => res.bytes(column)
- ).getOrElse(Bytes.empty)
-
- def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] =
- Properties.uncompress(read_bytes(db, name, column), cache = cache)
-
-
/* session info */
def session_info_exists(db: SQL.Database): Boolean = {
@@ -386,7 +419,10 @@
Store.Data.Session_Info.table.select(List(Store.Data.Session_Info.session_name),
sql = Store.Data.Session_Info.session_name.where_equal(name)))
- def clean_session_info(db: SQL.Database, name: String): Boolean =
+ def clean_session_info(db: SQL.Database, name: String): Boolean = {
+ Export.clean_session(db, name)
+ Document_Build.clean_session(db, name)
+
Store.Data.transaction_lock(db, create = true, synchronized = true) {
val already_defined = session_info_defined(db, name)
@@ -398,14 +434,9 @@
db.execute_statement(Store.Data.Sources.table.delete(
sql = Store.Data.Sources.where_equal(name)))
- db.execute_statement(
- Export.Data.Base.table.delete(sql = Export.Data.Base.session_name.where_equal(name)))
-
- db.execute_statement(
- Document_Build.Data.table.delete(sql = Document_Build.Data.session_name.where_equal(name)))
-
already_defined
}
+ }
def write_session_info(
db: SQL.Database,
@@ -420,48 +451,30 @@
}
}
- def read_session_timing(db: SQL.Database, name: String): Properties.T =
- Properties.decode(read_bytes(db, name, Store.Data.Session_Info.session_timing), cache = cache)
+ def read_session_timing(db: SQL.Database, session: String): Properties.T =
+ Store.Data.transaction_lock(db) { Store.Data.read_session_timing(db, session, cache) }
- def read_command_timings(db: SQL.Database, name: String): Bytes =
- read_bytes(db, name, Store.Data.Session_Info.command_timings)
-
- def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
- read_properties(db, name, Store.Data.Session_Info.theory_timings)
+ def read_command_timings(db: SQL.Database, session: String): Bytes =
+ Store.Data.transaction_lock(db) { Store.Data.read_command_timings(db, session) }
- def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
- read_properties(db, name, Store.Data.Session_Info.ml_statistics)
-
- def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] =
- read_properties(db, name, Store.Data.Session_Info.task_statistics)
+ def read_theory_timings(db: SQL.Database, session: String): List[Properties.T] =
+ Store.Data.transaction_lock(db) { Store.Data.read_theory_timings(db, session, cache) }
- def read_theories(db: SQL.Database, name: String): List[String] =
- read_theory_timings(db, name).flatMap(Markup.Name.unapply)
-
- def read_errors(db: SQL.Database, name: String): List[String] =
- Build_Log.uncompress_errors(read_bytes(db, name, Store.Data.Session_Info.errors), cache = cache)
+ def read_ml_statistics(db: SQL.Database, session: String): List[Properties.T] =
+ Store.Data.transaction_lock(db) { Store.Data.read_ml_statistics(db, session, cache) }
- def read_build(db: SQL.Database, name: String): Option[Store.Build_Info] = {
- if (db.tables.contains(Store.Data.Session_Info.table.name)) {
- db.execute_query_statementO[Store.Build_Info](
- Store.Data.Session_Info.table.select(
- sql = Store.Data.Session_Info.session_name.where_equal(name)),
- { res =>
- val uuid =
- try { Option(res.string(Store.Data.Session_Info.uuid)).getOrElse("") }
- catch { case _: SQLException => "" }
- Store.Build_Info(
- SHA1.fake_shasum(res.string(Store.Data.Session_Info.sources)),
- SHA1.fake_shasum(res.string(Store.Data.Session_Info.input_heaps)),
- SHA1.fake_shasum(res.string(Store.Data.Session_Info.output_heap)),
- res.int(Store.Data.Session_Info.return_code),
- uuid)
- }
- )
- }
- else None
- }
+ def read_task_statistics(db: SQL.Database, session: String): List[Properties.T] =
+ Store.Data.transaction_lock(db) { Store.Data.read_task_statistics(db, session, cache) }
+
+ def read_theories(db: SQL.Database, session: String): List[String] =
+ read_theory_timings(db, session).flatMap(Markup.Name.unapply)
+
+ def read_errors(db: SQL.Database, session: String): List[String] =
+ Store.Data.transaction_lock(db) { Store.Data.read_errors(db, session, cache) }
+
+ def read_build(db: SQL.Database, session: String): Option[Store.Build_Info] =
+ Store.Data.transaction_lock(db) { Store.Data.read_build(db, session) }
def read_sources(db: SQL.Database, session: String, name: String = ""): List[Store.Source_File] =
- Store.Data.read_sources(db, cache.compress, session, name = name)
+ Store.Data.transaction_lock(db) { Store.Data.read_sources(db, session, name, cache.compress) }
}
--- a/src/Pure/Tools/build_process.scala Fri Jul 07 14:05:05 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Sat Jul 08 16:48:15 2023 +0200
@@ -288,7 +288,7 @@
old_data: Map[String, A]
): Map[String, A] = {
val dom = data_domain -- old_data.keysIterator
- val data = old_data -- old_data.keysIterator.filterNot(dom)
+ val data = old_data -- old_data.keysIterator.filterNot(data_domain)
if (dom.isEmpty) data
else data_iterator(dom).foldLeft(data) { case (map, a) => map + (a.name -> a) }
}
@@ -342,7 +342,7 @@
val start = SQL.Column.date("start")
val stop = SQL.Column.date("stop")
- val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
+ val table = make_table(List(build_uuid, ml_platform, options, start, stop))
}
def read_builds(db: SQL.Database, build_uuid: String = ""): List[Build] = {
@@ -413,9 +413,11 @@
val old_command_timings = SQL.Column.bytes("old_command_timings")
val build_uuid = Generic.build_uuid
- val table = make_table("sessions",
- List(name, deps, ancestors, options, sources, timeout,
- old_time, old_command_timings, build_uuid))
+ val table =
+ make_table(
+ List(name, deps, ancestors, options, sources, timeout,
+ old_time, old_command_timings, build_uuid),
+ name = "sessions")
}
def read_sessions_domain(db: SQL.Database, build_uuid: String = ""): Set[String] =
@@ -485,7 +487,8 @@
val stop = SQL.Column.date("stop")
val serial = SQL.Column.long("serial")
- val table = make_table("workers", List(worker_uuid, build_uuid, start, stamp, stop, serial))
+ val table =
+ make_table(List(worker_uuid, build_uuid, start, stamp, stop, serial), name = "workers")
}
def read_serial(db: SQL.Database): Long =
@@ -575,7 +578,7 @@
val info = SQL.Column.string("info")
val build_uuid = Generic.build_uuid
- val table = make_table("pending", List(name, deps, info, build_uuid))
+ val table = make_table(List(name, deps, info, build_uuid), name = "pending")
}
def read_pending(db: SQL.Database): List[Task] =
@@ -622,7 +625,8 @@
val hostname = SQL.Column.string("hostname")
val numa_node = SQL.Column.int("numa_node")
- val table = make_table("running", List(name, worker_uuid, build_uuid, hostname, numa_node))
+ val table =
+ make_table(List(name, worker_uuid, build_uuid, hostname, numa_node), name = "running")
}
def read_running(db: SQL.Database): State.Running =
@@ -683,9 +687,10 @@
val current = SQL.Column.bool("current")
val table =
- make_table("results",
+ make_table(
List(name, worker_uuid, build_uuid, hostname, numa_node,
- rc, out, err, timing_elapsed, timing_cpu, timing_gc, output_shasum, current))
+ rc, out, err, timing_elapsed, timing_cpu, timing_gc, output_shasum, current),
+ name = "results")
}
def read_results_domain(db: SQL.Database): Set[String] =
@@ -728,8 +733,12 @@
)
def update_results(db: SQL.Database, results: State.Results): Boolean = {
- val old_results = read_results_domain(db)
- val insert = results.valuesIterator.filterNot(res => old_results.contains(res.name)).toList
+ val insert =
+ if (results.isEmpty) Nil
+ else {
+ val old_results = read_results_domain(db)
+ results.valuesIterator.filterNot(res => old_results.contains(res.name)).toList
+ }
for (result <- insert) {
val process_result = result.process_result
@@ -845,12 +854,12 @@
private val _build_database: Option[SQL.Database] =
try {
for (db <- store.maybe_open_build_database()) yield {
- val more_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
+ val store_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
Build_Process.Data.transaction_lock(db, create = true) {
Build_Process.Data.clean_build(db)
- more_tables.lock(db, create = true)
+ store_tables.lock(db, create = true)
}
- Build_Process.Data.vacuum(db, more_tables = more_tables)
+ db.vacuum(Build_Process.Data.tables ::: store_tables)
db
}
}