# HG changeset patch
# User wenzelm
# Date 1691692237 -7200
# Node ID 8f45302a9ff07ad4e042cbfdf02470764ff0fea8
# Parent  146468e05dd435c0ef703c48fccc5af3f966bbb0
more thorough ML_Heap.restore: include ancestors;                                                         prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;

diff -r 146468e05dd4 -r 8f45302a9ff0 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Thu Aug 10 19:58:23 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Thu Aug 10 20:30:37 2023 +0200
@@ -77,11 +77,19 @@
         name = "slices_size")
     }
 
-    def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =
-      db.execute_query_statementO[String](
-        Base.table.select(List(Base.digest), sql = Generic.name.where_equal(name)),
-        _.string(Base.digest)
-      ).flatMap(proper_string).map(SHA1.fake_digest)
+    def get_entries(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] = {
+      require(names.nonEmpty)
+
+      db.execute_query_statement(
+        Base.table.select(List(Base.name, Base.digest),
+          sql = Generic.name.where_member(names)),
+        List.from[(String, String)],
+        res => res.string(Base.name) -> res.string(Base.digest)
+      ).flatMap({
+        case (_, "") => None
+        case (name, digest) => Some(name -> SHA1.fake_digest(digest))
+      }).toMap
+    }
 
     def read_entry(db: SQL.Database, name: String): List[Bytes] =
       db.execute_query_statement(
@@ -127,9 +135,9 @@
       private_data.clean_entry(db, session_name)
     }
 
-  def get_entry(db: SQL.Database, session_name: String): Option[SHA1.Digest] =
-    private_data.transaction_lock(db, create = true, label = "ML_Heap.get_entry") {
-      private_data.get_entry(db, session_name)
+  def get_entries(db: SQL.Database, names: Iterable[String]): Map[String, SHA1.Digest] =
+    private_data.transaction_lock(db, create = true, label = "ML_Heap.get_entries") {
+      private_data.get_entries(db, names)
     }
 
   def store(
@@ -181,33 +189,35 @@
 
   def restore(
     database: Option[SQL.Database],
-    session_name: String,
-    heap: Path,
+    heaps: List[Path],
     cache: Compress.Cache = Compress.Cache.none
   ): Unit = {
     database match {
-      case None =>
-      case Some(db) =>
+      case Some(db) if heaps.nonEmpty =>
         private_data.transaction_lock(db, create = true, label = "ML_Heap.restore") {
-          val db_digest = private_data.get_entry(db, session_name)
-          val file_digest = read_file_digest(heap)
-
-          if (db_digest.isDefined && db_digest != file_digest) {
-            val base_dir = Isabelle_System.make_directory(heap.expand.dir)
-            Isabelle_System.with_tmp_file(session_name + "_", base_dir = base_dir.file) { tmp =>
-              Bytes.write(tmp, Bytes.empty)
-              for (slice <- private_data.read_entry(db, session_name)) {
-                Bytes.append(tmp, slice.uncompress(cache = cache))
+          val db_digests = private_data.get_entries(db, heaps.map(_.file_name))
+          for (heap <- heaps) {
+            val session_name = heap.file_name
+            val file_digest = read_file_digest(heap)
+            val db_digest = db_digests.get(session_name)
+            if (db_digest.isDefined && db_digest != file_digest) {
+              val base_dir = Isabelle_System.make_directory(heap.expand.dir)
+              Isabelle_System.with_tmp_file(session_name + "_", base_dir = base_dir.file) { tmp =>
+                Bytes.write(tmp, Bytes.empty)
+                for (slice <- private_data.read_entry(db, session_name)) {
+                  Bytes.append(tmp, slice.uncompress(cache = cache))
+                }
+                val digest = write_file_digest(tmp)
+                if (db_digest.get == digest) {
+                  Isabelle_System.chmod("a+r", tmp)
+                  Isabelle_System.move_file(tmp, heap)
+                }
+                else error("Incoherent content for session heap " + quote(session_name))
               }
-              val digest = write_file_digest(tmp)
-              if (db_digest.get == digest) {
-                Isabelle_System.chmod("a+r", tmp)
-                Isabelle_System.move_file(tmp, heap)
-              }
-              else error("Incoherent content for session heap " + quote(session_name))
             }
           }
         }
+      case _ =>
     }
   }
 }
diff -r 146468e05dd4 -r 8f45302a9ff0 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Thu Aug 10 19:58:23 2023 +0200
+++ b/src/Pure/Thy/store.scala	Thu Aug 10 20:30:37 2023 +0200
@@ -271,8 +271,15 @@
         cat_lines(input_dirs.map(dir => "  " + File.standard_path(dir))))
 
   def heap_shasum(database_server: Option[SQL.Database], name: String): SHA1.Shasum = {
-    def get_database = database_server.flatMap(ML_Heap.get_entry(_, name))
-    def get_file = find_heap(name).flatMap(ML_Heap.read_file_digest)
+    def get_database: Option[SHA1.Digest] = {
+      for {
+        db <- database_server
+        digest <- ML_Heap.get_entries(db, List(name)).valuesIterator.nextOption()
+      } yield digest
+    }
+
+    def get_file: Option[SHA1.Digest] =
+      find_heap(name).flatMap(ML_Heap.read_file_digest)
 
     get_database orElse get_file match {
       case Some(digest) => SHA1.shasum(digest, name)
diff -r 146468e05dd4 -r 8f45302a9ff0 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Thu Aug 10 19:58:23 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Thu Aug 10 20:30:37 2023 +0200
@@ -995,8 +995,8 @@
     val cancelled = progress.stopped || !ancestor_results.forall(_.ok)
 
     if (!skipped && !cancelled) {
-      ML_Heap.restore(_database_server, session_name, store.output_heap(session_name),
-        cache = store.cache.compress)
+      val heaps = (session_name :: ancestor_results.map(_.name)).map(store.output_heap)
+      ML_Heap.restore(_database_server, heaps, cache = store.cache.compress)
     }
 
     val result_name = (session_name, worker_uuid, build_uuid)