clarified init_database vs. update_database: implicitly assume fresh "instance";
authorwenzelm
Sun, 26 Feb 2023 19:14:47 +0100
changeset 77379 bd0028d1ece6
parent 77378 f047804f4860
child 77380 b9d9658131b0
clarified init_database vs. update_database: implicitly assume fresh "instance";
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Feb 26 18:52:33 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sun Feb 26 19:14:47 2023 +0100
@@ -443,8 +443,6 @@
       }
 
     def write_state(db: SQL.Database, instance: String, serial: Long, numa_index: Int): Unit = {
-      db.using_statement(
-        State.table.delete() + SQL.where(Generic.sql_equal(instance = instance)))(_.execute())
       db.using_statement(State.table.insert()) { stmt =>
         stmt.string(1) = instance
         stmt.long(2) = serial
@@ -453,6 +451,10 @@
       }
     }
 
+    def reset_state(db: SQL.Database, instance: String): Unit =
+      db.using_statement(
+        State.table.delete() + SQL.where(Generic.sql_equal(instance = instance)))(_.execute())
+
     def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = {
       val tables =
         List(Config.table, State.table, Pending.table, Running.table, Results.table)
@@ -478,7 +480,10 @@
 
       val (serial0, numa_index0) = read_state(db, instance)
       val serial = if (ch1 || ch2 || ch3) serial0 + 1 else serial0
-      if (serial != serial0) write_state(db, instance, serial, state.numa_index)
+      if (serial != serial0) {
+        reset_state(db, instance)
+        write_state(db, instance, serial, state.numa_index)
+      }
 
       state.copy(serial = serial)
     }