tuned;

--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:19:36 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 13:24:26 2024 +0100
@@ -187,15 +187,11 @@
     cache: Compress.Cache = Compress.Cache.none,
     progress: Progress = new Progress
   ): Unit = {
-    val size =
-      session.heap match {
-        case Some(heap) => File.size(heap) - sha1_prefix.length - SHA1.digest_length
-        case None => 0L
-      }
-
-    val slice_size = slice.bytes max Space.MiB(1).bytes
-    val slices = (size.toDouble / slice_size.toDouble).ceil.toInt
-    val step = if (slices > 0) (size.toDouble / slices.toDouble).ceil.toLong else 0L
+    val log_db =
+      for {
+        path <- session.log_db
+        uuid <- proper_string(Store.read_build_uuid(path, session.name))
+      } yield Log_DB(uuid, Bytes.read(path))
 
     val heap_digest =
       for {
@@ -203,11 +199,14 @@
         digest <- read_file_digest(path)
       } yield digest
 
-    val log_db =
-      for {
-        path <- session.log_db
-        uuid <- proper_string(Store.read_build_uuid(path, session.name))
-      } yield Log_DB(uuid, Bytes.read(path))
+    val heap_size =
+      session.heap match {
+        case Some(heap) => File.size(heap) - sha1_prefix.length - SHA1.digest_length
+        case None => 0L
+      }
+
+    val slice_size = slice.bytes max Space.MiB(1).bytes
+    val slices = (heap_size.toDouble / slice_size.toDouble).ceil.toInt
 
     try {
       if (slices == 0 && log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
@@ -218,10 +217,11 @@
 
       if (slices > 0) {
         progress.echo("Storing " + session.name + " ...")
+        val step = (heap_size.toDouble / slices.toDouble).ceil.toLong
         for (i <- 0 until slices) {
           val j = i + 1
           val offset = step * i
-          val limit = if (j < slices) step * j else size
+          val limit = if (j < slices) step * j else heap_size
           val content =
             Bytes.read_file(session.the_heap, offset = offset, limit = limit)
               .compress(cache = cache)
@@ -233,7 +233,7 @@
         if (log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...")
 
         private_data.transaction_lock(db, label = "ML_Heap.store3") {
-          private_data.finish_entry(db, session.name, size, heap_digest, log_db)
+          private_data.finish_entry(db, session.name, heap_size, heap_digest, log_db)
         }
       }
     }