# HG changeset patch
# User wenzelm
# Date 1687353658 -7200
# Node ID fd68b98de1f6e459e2ac2be38a4be5fe453cb4b7
# Parent  2df0f3604a6721c57988c90a56e1fe741b80bc87
prefer system option;

diff -r 2df0f3604a67 -r fd68b98de1f6 etc/options
--- a/etc/options	Wed Jun 21 14:27:51 2023 +0200
+++ b/etc/options	Wed Jun 21 15:20:58 2023 +0200
@@ -195,6 +195,9 @@
 option build_database_test : bool = false
   -- "expose state of build process via central database"
 
+option build_database_slice : real = 50.0
+  -- "slice size in MiB for ML heap stored within database"
+
 
 section "Editor Session"
 
diff -r 2df0f3604a67 -r fd68b98de1f6 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Wed Jun 21 14:27:51 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Wed Jun 21 15:20:58 2023 +0200
@@ -114,8 +114,8 @@
   def write_digest(
     database: Option[SQL.Database],
     heap: Path,
+    slice: Long,
     cache: Compress.Cache = Compress.Cache.none,
-    slice_size: Long = Space.MiB(50).bytes
   ): SHA1.Digest = {
     val digest = write_file_digest(heap)
     database match {
@@ -123,7 +123,7 @@
         val name = heap.file_name
         val size = File.space(heap).bytes - sha1_prefix.length - SHA1.digest_length
 
-        val slices = (size.toDouble / slice_size.toDouble).ceil.toInt
+        val slices = (size.toDouble / slice.toDouble).ceil.toInt
         val step = (size.toDouble / slices.toDouble).ceil.toLong
 
         try {
diff -r 2df0f3604a67 -r fd68b98de1f6 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Jun 21 14:27:51 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Wed Jun 21 15:20:58 2023 +0200
@@ -453,8 +453,11 @@
           val heap = store.output_heap(session_name)
           if (process_result.ok && store_heap && heap.is_file) {
             val database = store.maybe_open_heaps_database()
-            try { SHA1.shasum(ML_Heap.write_digest(database, heap), session_name) }
-            finally { database.foreach(_.close()) }
+            val slice = Space.MiB(options.real("build_database_slice")).bytes
+            val digest =
+              try { ML_Heap.write_digest(database, heap, slice = slice) }
+              finally { database.foreach(_.close()) }
+            SHA1.shasum(digest, session_name)
           }
           else SHA1.no_shasum
         }