# HG changeset patch
# User wenzelm
# Date 1708339671 -3600
# Node ID 5979ba12752478697fbfb207ba7d2f26c6643c7c
# Parent  49370f0f79113019700ad2e3405d4c3e8b67a022
clarified signature;
more robust slice_size;

diff -r 49370f0f7911 -r 5979ba127524 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Mon Feb 19 11:39:15 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Mon Feb 19 11:47:51 2024 +0100
@@ -470,7 +470,7 @@
           val output_shasum = {
             val heap = store.output_heap(session_name)
             if (process_result.ok && store_heap && heap.is_file) {
-              val slice = Space.MiB(options.real("build_database_slice")).bytes
+              val slice = Space.MiB(options.real("build_database_slice"))
               val digest = ML_Heap.store(database_server, session_name, heap, slice)
               SHA1.shasum(digest, session_name)
             }
diff -r 49370f0f7911 -r 5979ba127524 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Mon Feb 19 11:39:15 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Mon Feb 19 11:47:51 2024 +0100
@@ -144,7 +144,7 @@
     database: Option[SQL.Database],
     session_name: String,
     heap: Path,
-    slice: Long,
+    slice: Space,
     cache: Compress.Cache = Compress.Cache.none
   ): SHA1.Digest = {
     val digest = write_file_digest(heap)
@@ -153,8 +153,9 @@
       case Some(db) =>
         val size = File.size(heap) - sha1_prefix.length - SHA1.digest_length
 
-        val slices = (size.toDouble / slice.toDouble).ceil.toInt
-        val step = (size.toDouble / slices.toDouble).ceil.toLong
+        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
 
         try {
           private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") {