# HG changeset patch
# User wenzelm
# Date 1677696105 -3600
# Node ID 4fec9413f14be396b149a1c947d225569f4fc53e
# Parent  ce53c1ce85368c0b0403b3589c397d4efe56a842
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);

diff -r ce53c1ce8536 -r 4fec9413f14b src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 19:30:35 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 19:41:45 2023 +0100
@@ -471,7 +471,7 @@
             if (process_result.timeout) build_log.error("Timeout") else build_log,
           build =
             Sessions.Build_Info(sources_shasum, input_heaps, output_heap,
-              process_result.rc, UUID.random().toString)))
+              process_result.rc, build_context.uuid)))
 
       // messages
       process_result.err_lines.foreach(progress.echo)
diff -r ce53c1ce8536 -r 4fec9413f14b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 19:30:35 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 19:41:45 2023 +0100
@@ -28,7 +28,7 @@
       no_build: Boolean = false,
       verbose: Boolean = false,
       session_setup: (String, Session) => Unit = (_, _) => (),
-      instance: String = UUID.random().toString
+      uuid: String = UUID.random().toString
     ): Context = {
       val sessions_structure = build_deps.sessions_structure
       val build_graph = sessions_structure.build_graph
@@ -78,14 +78,14 @@
         }
 
       val numa_nodes = NUMA.nodes(enabled = numa_shuffling)
-      new Context(instance, store, build_deps, sessions, ordering, progress, hostname, numa_nodes,
+      new Context(uuid, store, build_deps, sessions, ordering, progress, hostname, numa_nodes,
         build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
         no_build = no_build, verbose = verbose, session_setup)
     }
   }
 
   final class Context private(
-    val instance: String,
+    val uuid: String,
     val store: Sessions.Store,
     val build_deps: Sessions.Deps,
     val sessions: Map[String, Build_Job.Session_Context],
@@ -200,26 +200,26 @@
       SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body)
 
     object Generic {
-      val instance = SQL.Column.string("instance")
+      val uuid = SQL.Column.string("uuid")
       val name = SQL.Column.string("name")
 
-      def sql_equal(instance: String = "", name: String = ""): SQL.Source =
+      def sql_equal(uuid: String = "", name: String = ""): SQL.Source =
         SQL.and(
-          if_proper(instance, Generic.instance.equal(instance)),
+          if_proper(uuid, Generic.uuid.equal(uuid)),
           if_proper(name, Generic.name.equal(name)))
 
-      def sql_member(instance: String = "", names: Iterable[String] = Nil): SQL.Source =
+      def sql_member(uuid: String = "", names: Iterable[String] = Nil): SQL.Source =
         SQL.and(
-          if_proper(instance, Generic.instance.equal(instance)),
+          if_proper(uuid, Generic.uuid.equal(uuid)),
           if_proper(names, Generic.name.member(names)))
     }
 
     object Base {
-      val instance = Generic.instance.make_primary_key
+      val uuid = Generic.uuid.make_primary_key
       val ml_platform = SQL.Column.string("ml_platform")
       val options = SQL.Column.string("options")
 
-      val table = make_table("", List(instance, ml_platform, options))
+      val table = make_table("", List(uuid, ml_platform, options))
     }
 
     object Serial {
@@ -441,7 +441,7 @@
       for (table <- tables) db.using_statement(table.delete())(_.execute())
 
       db.using_statement(Base.table.insert()) { stmt =>
-        stmt.string(1) = build_context.instance
+        stmt.string(1) = build_context.uuid
         stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM")
         stmt.string(3) = build_context.store.options.make_prefs(Options.init(prefs = ""))
         stmt.execute()
@@ -450,7 +450,7 @@
 
     def update_database(
       db: SQL.Database,
-      instance: String,
+      uuid: String,
       hostname: String,
       state: State
     ): State = {
@@ -520,7 +520,7 @@
         db.transaction {
           _state =
             Build_Process.Data.update_database(
-              db, build_context.instance, build_context.hostname, _state)
+              db, build_context.uuid, build_context.hostname, _state)
         }
       }
     }