clarified signature;
authorwenzelm
Mon, 19 Feb 2024 11:47:51 +0100
changeset 79678 5979ba127524
parent 79677 49370f0f7911
child 79679 ba2c43592f35
clarified signature; more robust slice_size;
src/Pure/Build/build_job.scala
src/Pure/ML/ml_heap.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)
             }
--- 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") {