--- 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") {