proper build_uuid for Build_Process.Task: thus old entries are removed via prepare_database/clean_build;
authorwenzelm
Tue, 14 Mar 2023 20:01:05 +0100
changeset 77661 45bd5c26cbcc
parent 77660 57fdb6c846b0
child 77662 b45fc98d11ea
proper build_uuid for Build_Process.Task: thus old entries are removed via prepare_database/clean_build;
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Mar 14 19:41:16 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Mar 14 20:01:05 2023 +0100
@@ -169,7 +169,8 @@
   case class Task(
     name: String,
     deps: List[String],
-    info: JSON.Object.T = JSON.Object.empty
+    info: JSON.Object.T,
+    build_uuid: String
   ) {
     def is_ready: Boolean = deps.isEmpty
     def resolve(dep: String): Task =
@@ -661,8 +662,9 @@
       val name = Generic.name.make_primary_key
       val deps = SQL.Column.string("deps")
       val info = SQL.Column.string("info")
+      val build_uuid = Generic.build_uuid
 
-      val table = make_table("pending", List(name, deps, info))
+      val table = make_table("pending", List(name, deps, info, build_uuid))
     }
 
     def read_pending(db: SQL.Database): List[Task] =
@@ -673,7 +675,8 @@
           val name = res.string(Pending.name)
           val deps = res.string(Pending.deps)
           val info = res.string(Pending.info)
-          Task(name, split_lines(deps), info = JSON.Object.parse(info))
+          val build_uuid = res.string(Pending.build_uuid)
+          Task(name, split_lines(deps), JSON.Object.parse(info), build_uuid)
         })
 
     def update_pending(db: SQL.Database, pending: State.Pending): Boolean = {
@@ -685,12 +688,13 @@
           Pending.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name)))))
       }
 
-      for (entry <- insert) {
+      for (task <- insert) {
         db.execute_statement(Pending.table.insert(), body =
           { stmt =>
-            stmt.string(1) = entry.name
-            stmt.string(2) = cat_lines(entry.deps)
-            stmt.string(3) = JSON.Format(entry.info)
+            stmt.string(1) = task.name
+            stmt.string(2) = cat_lines(task.deps)
+            stmt.string(3) = JSON.Format(task.info)
+            stmt.string(4) = task.build_uuid
           })
       }
 
@@ -1020,7 +1024,7 @@
         for {
           (name, session_context) <- build_context.sessions.iterator
           if !old_pending(name)
-        } yield Build_Process.Task(name, session_context.deps))
+        } yield Build_Process.Task(name, session_context.deps, JSON.Object.empty, build_uuid))
     val pending1 = new_pending ::: state.pending
 
     state.copy(sessions = sessions1, pending = pending1)