# HG changeset patch # User wenzelm # Date 1688814790 -7200 # Node ID d8c99a497502c69c8dbea4b94606faa163623a24 # Parent 03eb7f7bb990f6bf7248acd58d0c1c7406590617 clarified signature; diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Fri Jul 07 18:04:45 2023 +0200 +++ b/src/Pure/Admin/build_log.scala Sat Jul 08 13:13:10 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)) } } diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/General/sql.scala --- a/src/Pure/General/sql.scala Fri Jul 07 18:04:45 2023 +0200 +++ b/src/Pure/General/sql.scala Sat Jul 08 13:13:10 2023 +0200 @@ -259,7 +259,7 @@ if (synchronized) db.synchronized { run } else run } - 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") diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/ML/ml_heap.scala --- a/src/Pure/ML/ml_heap.scala Fri Jul 07 18:04:45 2023 +0200 +++ b/src/Pure/ML/ml_heap.scala Sat Jul 08 13:13:10 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] = diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/System/host.scala --- a/src/Pure/System/host.scala Fri Jul 07 18:04:45 2023 +0200 +++ b/src/Pure/System/host.scala Sat Jul 08 13:13:10 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 = diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Fri Jul 07 18:04:45 2023 +0200 +++ b/src/Pure/System/progress.scala Sat Jul 08 13:13:10 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] = diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Fri Jul 07 18:04:45 2023 +0200 +++ b/src/Pure/Thy/document_build.scala Sat Jul 08 13:13:10 2023 +0200 @@ -64,7 +64,7 @@ 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)) + val table = make_table(List(session_name, name, sources, log_xz, pdf)) } def where_equal(session_name: String, name: String = ""): SQL.Source = diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Fri Jul 07 18:04:45 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Sat Jul 08 13:13:10 2023 +0200 @@ -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] =