# HG changeset patch
# User wenzelm
# Date 1677435287 -3600
# Node ID bd0028d1ece6f4afa8117a286333c0dc3c4b9c70
# Parent  f047804f48602df3d9173030e812852c6c03e3ca
clarified init_database vs. update_database: implicitly assume fresh "instance";

diff -r f047804f4860 -r bd0028d1ece6 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)
     }