clarified store_session: heap requires process_result.ok, but log_db is always stored;
clarified ML_Heap.clean_entry vs. ML_Heap.init_entry;

--- a/src/Pure/Build/build_job.scala	Thu Feb 22 12:22:13 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Thu Feb 22 12:53:07 2024 +0100
@@ -120,7 +120,6 @@
         val options = Host.node_options(info.options, node_info)
 
         val store = build_context.store
-        val store_session = store.output_session(session_name, store_heap = store_heap)
 
         using_optional(store.maybe_open_database_server(server = server)) { database_server =>
 
@@ -465,14 +464,16 @@
             else if (result2.interrupted) result2.error(Output.error_message_text("Interrupt"))
             else result2
 
+          val store_session =
+            store.output_session(session_name, store_heap = process_result.ok && store_heap)
+
 
           /* output heap */
 
           val output_shasum =
             store_session.heap match {
-              case Some(path) if process_result.ok =>
-                SHA1.shasum(ML_Heap.write_file_digest(path), session_name)
-              case _ => SHA1.no_shasum
+              case Some(path) => SHA1.shasum(ML_Heap.write_file_digest(path), session_name)
+              case None => SHA1.no_shasum
             }
 
           val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test)
@@ -517,11 +518,8 @@
           using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
             heaps_database =>
               for (db <- database_server orElse heaps_database) {
-                ML_Heap.clean_entry(db, session_name)
-                if (process_result.ok) {
-                  val slice = Space.MiB(options.real("build_database_slice"))
-                  ML_Heap.store(db, store_session, slice, progress = progress)
-                }
+                val slice = Space.MiB(options.real("build_database_slice"))
+                ML_Heap.store(db, store_session, slice, progress = progress)
               }
           }
 

--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 12:22:13 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 12:53:07 2024 +0100
@@ -131,12 +131,13 @@
       for (table <- List(Base.table, Slices.table)) {
         db.execute_statement(table.delete(sql = Base.name.where_equal(name)))
       }
+    }
+
+    def init_entry(db: SQL.Database, name: String): Unit = {
+      clean_entry(db, name)
       for (table <- List(Size.table, Slices_Size.table)) {
         db.create_view(table)
       }
-    }
-
-    def init_entry(db: SQL.Database, name: String): Unit =
       db.execute_statement(Base.table.insert(), body =
         { stmt =>
           stmt.string(1) = name
@@ -145,6 +146,7 @@
           stmt.string(4) = None
           stmt.bytes(5) = None
         })
+    }
 
     def finish_entry(
       db: SQL.Database,