# HG changeset patch
# User wenzelm
# Date 1687520854 -7200
# Node ID 140a6f2e3728c6776d640bc9d62aa6bbe5386f97
# Parent  93266b0340f8552f322ee306c253ae1eb709fb00
restore heaps from database, which takes precedence over file-system;

diff -r 93266b0340f8 -r 140a6f2e3728 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Fri Jun 23 11:14:44 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Fri Jun 23 13:47:34 2023 +0200
@@ -70,12 +70,18 @@
       db.execute_query_statementB(
         Base.table.select(List(Base.name), sql = Base.name.where_equal(name)))
 
-    def defined_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =
+    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 read_entry(db: SQL.Database, name: String): List[Bytes] =
+      db.execute_query_statement(
+        Slices.table.select(List(Slices.content),
+          sql = Generic.name.where_equal(name) + SQL.order_by(List(Slices.slice))),
+        List.from[Bytes], _.bytes(Slices.content))
+
     def clean_entry(db: SQL.Database, name: String): Unit = {
       for (table <- List(Base.table, Slices.table)) {
         db.execute_statement(table.delete(sql = Base.name.where_equal(name)))
@@ -111,6 +117,9 @@
   def clean_entry(db: SQL.Database, name: String): Unit =
     Data.transaction_lock(db, create = true) { Data.clean_entry(db, name) }
 
+  def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =
+    Data.transaction_lock(db, create = true) { Data.get_entry(db, name) }
+
   def store(
     database: Option[SQL.Database],
     heap: Path,
@@ -149,4 +158,26 @@
     }
     digest
   }
+
+  def restore(
+    db: SQL.Database,
+    heap: Path,
+    cache: Compress.Cache = Compress.Cache.none
+  ): Unit = {
+    val name = heap.file_name
+    Data.transaction_lock(db, create = true) {
+      val db_digest = Data.get_entry(db, name)
+      val file_digest = read_file_digest(heap)
+
+      if (db_digest.isDefined && db_digest != file_digest) {
+        Isabelle_System.make_directory(heap.expand.dir)
+        Bytes.write(heap, Bytes.empty)
+          for (slice <- Data.read_entry(db, name)) {
+            Bytes.append(heap, slice.uncompress(cache = cache))
+          }
+        val digest = write_file_digest(heap)
+        if (db_digest.get != digest) error("Incoherent content for file " + heap)
+      }
+    }
+  }
 }
diff -r 93266b0340f8 -r 140a6f2e3728 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Fri Jun 23 11:14:44 2023 +0200
+++ b/src/Pure/Thy/store.scala	Fri Jun 23 13:47:34 2023 +0200
@@ -227,17 +227,21 @@
   def find_heap(name: String): Option[Path] =
     input_dirs.map(_ + heap(name)).find(_.is_file)
 
-  def find_heap_shasum(name: String): SHA1.Shasum =
-    (for {
-      path <- find_heap(name)
-      digest <- ML_Heap.read_file_digest(path)
-    } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum)
-
   def the_heap(name: String): Path =
     find_heap(name) getOrElse
       error("Missing heap image for session " + quote(name) + " -- expected in:\n" +
         cat_lines(input_dirs.map(dir => "  " + File.standard_path(dir))))
 
+  def heap_shasum(database: Option[SQL.Database], name: String): SHA1.Shasum = {
+    def get_database = database.flatMap(ML_Heap.get_entry(_, name))
+    def get_file = find_heap(name).flatMap(ML_Heap.read_file_digest)
+
+    get_database orElse get_file match {
+      case Some(digest) => SHA1.shasum(digest, name)
+      case None => SHA1.no_shasum
+    }
+  }
+
 
   /* databases for build process and session content */
 
@@ -333,18 +337,20 @@
   ): (Boolean, SHA1.Shasum) = {
     try_open_database(name) match {
       case Some(db) =>
-        using(db)(read_build(_, name)) match {
-          case Some(build) =>
-            val output_shasum = find_heap_shasum(name)
-            val current =
-              !fresh_build &&
-              build.ok &&
-              Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
-              build.input_heaps == input_shasum &&
-              build.output_heap == output_shasum &&
-              !(store_heap && output_shasum.is_empty)
-            (current, output_shasum)
-          case None => (false, SHA1.no_shasum)
+        using(db) { _ =>
+          read_build(db, name) match {
+            case Some(build) =>
+              val output_shasum = heap_shasum(if (db.is_postgresql) Some(db) else None, name)
+              val current =
+                !fresh_build &&
+                  build.ok &&
+                  Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
+                  build.input_heaps == input_shasum &&
+                  build.output_heap == output_shasum &&
+                  !(store_heap && output_shasum.is_empty)
+              (current, output_shasum)
+            case None => (false, SHA1.no_shasum)
+          }
         }
       case None => (false, SHA1.no_shasum)
     }
diff -r 93266b0340f8 -r 140a6f2e3728 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Fri Jun 23 11:14:44 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jun 23 13:47:34 2023 +0200
@@ -905,6 +905,16 @@
     val skipped = build_context.no_build
     val cancelled = progress.stopped || !ancestor_results.forall(_.ok)
 
+    if (!skipped && !cancelled) {
+      val database = store.maybe_open_heaps_database()
+      try {
+        for (db <- database) {
+          ML_Heap.restore(db, store.output_heap(session_name), cache = store.cache.compress)
+        }
+      }
+      finally { database.foreach(_.close()) }
+    }
+
     val result_name = (session_name, worker_uuid, build_uuid)
 
     if (finished) {