# HG changeset patch
# User paulson
# Date 1713388041 -3600
# Node ID 8262d4f63b58844651b406547a2b7403633a83f6
# Parent  2fe244c4bb010d125bd0eae681791204ee2a1d4d# Parent  601ff5c7cad5b9e2d1615e2f132b658896cf389f
merged

diff -r 601ff5c7cad5 -r 8262d4f63b58 src/HOL/Data_Structures/Selection.thy
--- a/src/HOL/Data_Structures/Selection.thy	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/HOL/Data_Structures/Selection.thy	Wed Apr 17 22:07:21 2024 +0100
@@ -310,6 +310,12 @@
         if y < x then (y # ls, es, gs) else if x = y then (ls, y # es, gs) else (ls, es, y # gs))"
   by (auto simp: partition3_def)
 
+lemma length_partition3:
+  assumes "partition3 x xs = (ls, es, gs)"
+  shows   "length xs = length ls + length es + length gs"
+  using assms by (induction xs arbitrary: ls es gs)
+                 (auto simp: partition3_code split: if_splits prod.splits)
+
 lemma sort_append:
   assumes "\<forall>x\<in>set xs. \<forall>y\<in>set ys. x \<le> y"
   shows   "sort (xs @ ys) = sort xs @ sort ys"
@@ -643,19 +649,39 @@
 definition T_slow_median :: "'a :: linorder list \<Rightarrow> nat" where
   "T_slow_median xs = T_length xs + T_slow_select ((length xs - 1) div 2) xs"
 
-lemma T_slow_select_le: "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 2"
+lemma T_slow_select_le:
+  assumes "k < length xs"
+  shows   "T_slow_select k xs \<le> length xs ^ 2 + 3 * length xs + 1"
 proof -
-  have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (insort xs) + 1)"
-    unfolding T_slow_select_def
-    by (intro add_mono T_insort_length) (auto simp: T_nth_eq)
-  also have "\<dots> = length xs ^ 2 + 3 * length xs + 2"
-    by (simp add: insort_correct algebra_simps power2_eq_square)
-  finally show ?thesis .
+  have "T_slow_select k xs = T_insort xs + T_nth (Sorting.insort xs) k"
+    unfolding T_slow_select_def ..
+  also have "T_insort xs \<le> (length xs + 1) ^ 2"
+    by (rule T_insort_length)
+  also have "T_nth (Sorting.insort xs) k = k + 1"
+    using assms by (subst T_nth_eq) (auto simp: length_insort)
+  also have "k + 1 \<le> length xs"
+    using assms by linarith
+  also have "(length xs + 1) ^ 2 + length xs = length xs ^ 2 + 3 * length xs + 1"
+    by (simp add: algebra_simps power2_eq_square)
+  finally show ?thesis by - simp_all
 qed
 
-lemma T_slow_median_le: "T_slow_median xs \<le> length xs ^ 2 + 4 * length xs + 3"
-  unfolding T_slow_median_def using T_slow_select_le[of "(length xs - 1) div 2" xs]
-  by (simp add: algebra_simps T_length_eq)
+lemma T_slow_median_le:
+  assumes "xs \<noteq> []"
+  shows   "T_slow_median xs \<le> length xs ^ 2 + 4 * length xs + 2"
+proof -
+  have "T_slow_median xs = length xs + T_slow_select ((length xs - 1) div 2) xs + 1"
+    by (simp add: T_slow_median_def T_length_eq)
+  also from assms have "length xs > 0"
+    by simp
+  hence "(length xs - 1) div 2 < length xs"
+    by linarith
+  hence "T_slow_select ((length xs - 1) div 2) xs \<le> length xs ^ 2 + 3 * length xs + 1"
+    by (intro T_slow_select_le) auto
+  also have "length xs + \<dots> + 1 = length xs ^ 2 + 4 * length xs + 2"
+    by (simp add: algebra_simps)
+  finally show ?thesis by - simp_all
+qed
 
 
 time_fun chop
@@ -717,16 +743,16 @@
 function T'_mom_select :: "nat \<Rightarrow> nat" where
   "T'_mom_select n =
      (if n \<le> 20 then
-        483
+        482
       else
-        T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 19 * n + 55)"
+        T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n+3\<rceil>) + 19 * n + 54)"
   by force+
 termination by (relation "measure id"; simp; linarith)
 
 lemmas [simp del] = T'_mom_select.simps
 
 
-lemma T'_mom_select_ge: "T'_mom_select n \<ge> 483"
+lemma T'_mom_select_ge: "T'_mom_select n \<ge> 482"
   by (induction n rule: T'_mom_select.induct; subst T'_mom_select.simps) auto
 
 lemma T'_mom_select_mono:
@@ -736,7 +762,7 @@
   show ?case
   proof (cases "m \<le> 20")
     case True
-    hence "T'_mom_select m = 483"
+    hence "T'_mom_select m = 482"
       by (subst T'_mom_select.simps) auto
     also have "\<dots> \<le> T'_mom_select n"
       by (rule T'_mom_select_ge)
@@ -744,9 +770,9 @@
   next
     case False
     hence "T'_mom_select m =
-             T'_mom_select (nat \<lceil>0.2*m\<rceil>) + T'_mom_select (nat \<lceil>0.7*m + 3\<rceil>) + 19 * m + 55"
+             T'_mom_select (nat \<lceil>0.2*m\<rceil>) + T'_mom_select (nat \<lceil>0.7*m + 3\<rceil>) + 19 * m + 54"
       by (subst T'_mom_select.simps) auto
-    also have "\<dots> \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + 19 * n + 55"
+    also have "\<dots> \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>) + T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + 19 * n + 54"
       using \<open>m \<le> n\<close> and False by (intro add_mono less.IH; linarith)
     also have "\<dots> = T'_mom_select n"
       using \<open>m \<le> n\<close> and False by (subst T'_mom_select.simps) auto
@@ -754,7 +780,10 @@
   qed
 qed
 
-lemma T_mom_select_le_aux: "T_mom_select k xs \<le> T'_mom_select (length xs)"
+lemma T_mom_select_le_aux:
+  assumes "k < length xs"
+  shows   "T_mom_select k xs \<le> T'_mom_select (length xs)"
+  using assms
 proof (induction k xs rule: T_mom_select.induct)
   case (1 k xs)
   define n where [simp]: "n = length xs"
@@ -771,11 +800,12 @@
   show ?case
   proof (cases "length xs \<le> 20")
     case True \<comment> \<open>base case\<close>
-    hence "T_mom_select k xs \<le> (length xs)\<^sup>2 + 4 * length xs + 3"
-      using T_slow_select_le[of k xs] by (subst T_mom_select.simps) (auto simp: T_length_eq)
-    also have "\<dots> \<le> 20\<^sup>2 + 4 * 20 + 3"
+    hence "T_mom_select k xs \<le> (length xs)\<^sup>2 + 4 * length xs + 2"
+      using T_slow_select_le[of k xs] \<open>k < length xs\<close>
+      by (subst T_mom_select.simps) (auto simp: T_length_eq)
+    also have "\<dots> \<le> 20\<^sup>2 + 4 * 20 + 2"
       using True by (intro add_mono power_mono) auto
-    also have "\<dots> = 483"
+    also have "\<dots> = 482"
       by simp
     also have "\<dots> = T'_mom_select (length xs)"
       using True by (simp add: T'_mom_select.simps)
@@ -794,34 +824,36 @@
 
     text \<open>The cost of computing the medians of all the subgroups:\<close>
     define T_ms where "T_ms = T_map T_slow_median (chop 5 xs)"
-    have "T_ms \<le> 10 * n + 49"
+    have "T_ms \<le> 10 * n + 48"
     proof -
       have "T_ms = (\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) + length (chop 5 xs) + 1"
         by (simp add: T_ms_def T_map_eq)
-      also have "(\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) \<le> (\<Sum>ys\<leftarrow>chop 5 xs. 48)"
+      also have "(\<Sum>ys\<leftarrow>chop 5 xs. T_slow_median ys) \<le> (\<Sum>ys\<leftarrow>chop 5 xs. 47)"
       proof (intro sum_list_mono)
         fix ys assume "ys \<in> set (chop 5 xs)"
-        hence "length ys \<le> 5"
-          using length_chop_part_le by blast
-        have "T_slow_median ys \<le> (length ys) ^ 2 + 4 * length ys + 3"
+        hence "length ys \<le> 5" "ys \<noteq> []"
+          using length_chop_part_le[of ys 5 xs] by auto
+        from \<open>ys \<noteq> []\<close> have "T_slow_median ys \<le> (length ys) ^ 2 + 4 * length ys + 2"
           by (rule T_slow_median_le)
-        also have "\<dots> \<le> 5 ^ 2 + 4 * 5 + 3"
+        also have "\<dots> \<le> 5 ^ 2 + 4 * 5 + 2"
           using \<open>length ys \<le> 5\<close> by (intro add_mono power_mono) auto
-        finally show "T_slow_median ys \<le> 48" by simp
+        finally show "T_slow_median ys \<le> 47" by simp
       qed
-      also have "(\<Sum>ys\<leftarrow>chop 5 xs. 48) + length (chop 5 xs) + 1 =
-                   49 * nat \<lceil>real n / 5\<rceil> + 1"
+      also have "(\<Sum>ys\<leftarrow>chop 5 xs. 47) + length (chop 5 xs) + 1 =
+                   48 * nat \<lceil>real n / 5\<rceil> + 1"
         by (simp add: map_replicate_const length_chop)
-      also have "\<dots> \<le> 10 * n + 49"
+      also have "\<dots> \<le> 10 * n + 48"
         by linarith
-      finally show "T_ms \<le> 10 * n + 49" by simp
+      finally show "T_ms \<le> 10 * n + 48" by simp
     qed
 
     text \<open>The cost of the first recursive call (to compute the median of medians):\<close>
     define T_rec1 where
       "T_rec1 = T_mom_select (((length xs + 4) div 5 - 1) div 2) (map slow_median (chop 5 xs))"
-    have "T_rec1 \<le> T'_mom_select (length (map slow_median (chop 5 xs)))"
-      using False unfolding T_rec1_def by (intro IH(3)) auto
+    from False have "((length xs + 4) div 5 - Suc 0) div 2 < nat \<lceil>real (length xs) / 5\<rceil>"
+      by linarith
+    hence "T_rec1 \<le> T'_mom_select (length (map slow_median (chop 5 xs)))"
+      using False unfolding T_rec1_def by (intro IH(3)) (auto simp: length_chop)
     hence "T_rec1 \<le> T'_mom_select (nat \<lceil>0.2 * n\<rceil>)"
       by (simp add: length_chop)
 
@@ -855,7 +887,17 @@
       hence "T_rec2 = T_mom_select (k - nl - ne) gs"
         by (simp add: T_rec2_def)
       also have "\<dots> \<le> T'_mom_select (length gs)"
-        unfolding nl_def ne_def by (rule IH(2)) (use \<open>k \<ge> nl + ne\<close> False in \<open>auto simp: defs\<close>)
+        unfolding nl_def ne_def 
+      proof (rule IH(2))
+        show "\<not> length xs \<le> 20"
+          using False by auto
+        show "\<not> k < length ls" "\<not>k < length ls + length es"
+          using \<open>k \<ge> nl + ne\<close> by (auto simp: nl_def ne_def)
+        have "length xs = nl + ne + length gs"
+          unfolding defs by (rule length_partition3) (simp_all add: partition3_def)
+        thus "k - length ls - length es < length gs"
+          using \<open>k \<ge> nl + ne\<close> \<open>k < length xs\<close> by (auto simp: nl_def ne_def)
+      qed
       also have "length gs \<le> nat \<lceil>0.7 * n + 3\<rceil>"
         unfolding gs_def using size_greater_than_median_of_medians[of xs]
         by (auto simp: length_filter_conv_size_filter_mset slow_median_correct[abs_def] x_eq)
@@ -871,13 +913,13 @@
                         T_length_eq T_ms_def)
     also have "nl \<le> n" by (simp add: nl_def ls_def)
     also have "ne \<le> n" by (simp add: ne_def es_def)
-    also note \<open>T_ms \<le> 10 * n + 49\<close>
+    also note \<open>T_ms \<le> 10 * n + 48\<close>
     also have "T_chop 5 xs \<le> 5 * n + 1"
       using T_chop_le[of 5 xs] by simp 
     also note \<open>T_rec1 \<le> T'_mom_select (nat \<lceil>0.2*n\<rceil>)\<close>
     also note \<open>T_rec2 \<le> T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>)\<close>
     finally have "T_mom_select k xs \<le>
-                    T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + T'_mom_select (nat \<lceil>0.2*n\<rceil>) + 19 * n + 55"
+                    T'_mom_select (nat \<lceil>0.7*n + 3\<rceil>) + T'_mom_select (nat \<lceil>0.2*n\<rceil>) + 19 * n + 54"
       by simp
     also have "\<dots> = T'_mom_select n"
       using False by (subst T'_mom_select.simps) auto
@@ -1034,7 +1076,7 @@
 lemma T'_mom_select_le': "\<exists>C\<^sub>1 C\<^sub>2. \<forall>n. T'_mom_select n \<le> C\<^sub>1 * n + C\<^sub>2"
 proof (rule akra_bazzi_light_nat)
   show "\<forall>n>20. T'_mom_select n = T'_mom_select (nat \<lceil>0.2 * n + 0\<rceil>) +
-                 T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>) + 19 * n + 55"
+                 T'_mom_select (nat \<lceil>0.7 * n + 3\<rceil>) + 19 * n + 54"
     using T'_mom_select.simps by auto
 qed auto
 
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/HOL/Data_Structures/Time_Funs.thy
--- a/src/HOL/Data_Structures/Time_Funs.thy	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/HOL/Data_Structures/Time_Funs.thy	Wed Apr 17 22:07:21 2024 +0100
@@ -43,12 +43,9 @@
 
 lemmas [simp del] = T_filter.simps
 
+time_fun nth
 
-fun T_nth :: "'a list \<Rightarrow> nat \<Rightarrow> nat" where
-  "T_nth [] n = 1"
-| "T_nth (x # xs) n = (case n of 0 \<Rightarrow> 1 | Suc n' \<Rightarrow> T_nth xs n' + 1)"
-
-lemma T_nth_eq: "T_nth xs n = min n (length xs) + 1"
+lemma T_nth_eq: "n < length xs \<Longrightarrow> T_nth xs n = n + 1"
   by (induction xs n rule: T_nth.induct) (auto split: nat.splits)
 
 lemmas [simp del] = T_nth.simps
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/HOL/Library/adhoc_overloading.ML
--- a/src/HOL/Library/adhoc_overloading.ML	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/HOL/Library/adhoc_overloading.ML	Wed Apr 17 22:07:21 2024 +0100
@@ -154,7 +154,9 @@
 fun get_candidates ctxt (c, T) =
   get_variants ctxt c
   |> Option.map (map_filter (fn (t, T') =>
-    if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t
+    if unifiable_with (Proof_Context.theory_of ctxt) T T'
+    (*keep the type constraint for the type-inference check phase*)
+    then SOME (Type.constraint T t)
     else NONE));
 
 fun insert_variants ctxt t (oconst as Const (c, T)) =
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -34,8 +34,9 @@
     ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
     hostname: String = Isabelle_System.hostname(),
     numa_shuffling: Boolean = false,
+    numa_nodes: List[Int] = Nil,
     clean_sessions: List[String] = Nil,
-    build_heap: Boolean = false,
+    store_heap: Boolean = false,
     fresh_build: Boolean = false,
     no_build: Boolean = false,
     session_setup: (String, Session) => Unit = (_, _) => (),
@@ -78,10 +79,11 @@
     def cache: Term.Cache = store.cache
 
     def sessions_ok: List[String] =
-      (for {
-        name <- deps.sessions_structure.build_topological_order.iterator
-        result <- results.get(name) if result.ok
-      } yield name).toList
+      List.from(
+        for {
+          name <- deps.sessions_structure.build_topological_order.iterator
+          result <- results.get(name) if result.ok
+        } yield name)
 
     def info(name: String): Sessions.Info = deps.sessions_structure(name)
     def sessions: Set[String] = results.keySet
@@ -208,11 +210,9 @@
                 case Some(db) =>
                   using(db)(store.read_build(_, name)) match {
                     case Some(build) if build.ok =>
-                      val session_options = deps0.sessions_structure(name).options
-                      val session_sources = deps0.sources_shasum(name)
-                      if (Sessions.eq_sources(session_options, build.sources, session_sources)) {
-                        None
-                      }
+                      val sources_shasum = deps0.sources_shasum(name)
+                      val thorough = deps0.sessions_structure(name).build_thorough
+                      if (Sessions.eq_sources(thorough, build.sources, sources_shasum)) None
                       else Some(name)
                     case _ => Some(name)
                   }
@@ -230,10 +230,11 @@
 
       if (check_unknown_files) {
         val source_files =
-          (for {
-            (_, base) <- build_deps.session_bases.iterator
-            (path, _) <- base.session_sources.iterator
-          } yield path).toList
+          List.from(
+            for {
+              (_, base) <- build_deps.session_bases.iterator
+              (path, _) <- base.session_sources.iterator
+            } yield path)
         Mercurial.check_files(source_files)._2 match {
           case Nil =>
           case unknown_files =>
@@ -249,12 +250,13 @@
       val clean_sessions =
         if (clean_build) full_sessions.imports_descendants(full_sessions_selection) else Nil
 
+      val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
       val build_context =
         Context(store, build_deps, engine = engine, afp_root = afp_root,
           build_hosts = build_hosts, hostname = hostname(build_options),
-          clean_sessions = clean_sessions, build_heap = build_heap,
-          numa_shuffling = numa_shuffling, fresh_build = fresh_build,
-          no_build = no_build, session_setup = session_setup,
+          clean_sessions = clean_sessions, store_heap = build_heap,
+          numa_shuffling = numa_shuffling, numa_nodes = numa_nodes,
+          fresh_build = fresh_build, no_build = no_build, session_setup = session_setup,
           jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true)
 
       val results = engine.run_build_process(build_context, progress, server)
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -65,21 +65,11 @@
         benchmark_requirements(local_options, progress)
         for (db <- database_server) ML_Heap.restore(db, hierachy, cache = store.cache.compress)
 
-        def get_shasum(session_name: String): SHA1.Shasum = {
-          val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
-
-          val input_shasum =
-            if (ancestor_shasums.isEmpty) ML_Process.bootstrap_shasum()
-            else SHA1.flat_shasum(ancestor_shasums)
-
-          store.check_output(
-            database_server, session_name,
-            session_options = build_context.sessions_structure(session_name).options,
-            sources_shasum = sessions(session_name).sources_shasum,
-            input_shasum = input_shasum,
-            fresh_build = false,
-            store_heap = false)._2
-        }
+        def get_shasum(name: String): SHA1.Shasum =
+          store.check_output(database_server, name,
+            sources_shasum = sessions(name).sources_shasum,
+            input_shasum = ML_Process.make_shasum(sessions(name).ancestors.map(get_shasum)),
+            build_thorough = build_context.sessions_structure(name).build_thorough)._2
 
         val deps = Sessions.deps(full_sessions.selection(selection)).check_errors
         val background = deps.background(benchmark_session_name)
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_job.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -514,14 +514,8 @@
             case None => using(store.open_database(session_name, output = true))(write_info)
           }
 
-          using_optional(store.maybe_open_heaps_database(database_server, server = server)) {
-            heaps_database =>
-              for (db <- database_server orElse heaps_database) {
-                val slice = Space.MiB(options.real("build_database_slice"))
-                ML_Heap.store(db, store_session, slice,
-                  cache = store.cache.compress, progress = progress)
-              }
-          }
+          store.in_heaps_database(
+            List(store_session), database_server, server = server, progress = progress)
 
           // messages
           process_result.err_lines.foreach(progress.echo(_))
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -94,6 +94,9 @@
     def iterator: Iterator[Build_Job.Session_Context] =
       for (name <- graph.topological_order.iterator) yield apply(name)
 
+    def store_heap(name: String): Boolean =
+      isabelle.Sessions.is_pure(name) || iterator.exists(_.ancestors.contains(name))
+
     def data: Library.Update.Data[Build_Job.Session_Context] =
       Map.from(for ((_, (session, _)) <- graph.iterator) yield session.name -> session)
 
@@ -221,7 +224,6 @@
 
   sealed case class State(
     serial: Long = 0,
-    numa_nodes: List[Int] = Nil,
     sessions: Sessions = Sessions.empty,
     pending: State.Pending = Map.empty,
     running: State.Running = Map.empty,
@@ -1148,9 +1150,10 @@
   }
 
   protected def next_node_info(state: Build_Process.State, session_name: String): Host.Node_Info = {
-    def used_nodes: Set[Int] =
+    val available_nodes = build_context.numa_nodes
+    val used_nodes =
       Set.from(for (job <- state.running.valuesIterator; i <- job.node_info.numa_node) yield i)
-    val numa_node = Host.next_numa_node(_host_database, hostname, state.numa_nodes, used_nodes)
+    val numa_node = Host.next_numa_node(_host_database, hostname, available_nodes, used_nodes)
     Host.Node_Info(hostname, numa_node, Nil)
   }
 
@@ -1160,20 +1163,13 @@
     ancestor_results: List[Build_Process.Result]
   ): Build_Process.State = {
     val sources_shasum = state.sessions(session_name).sources_shasum
-
-    val input_shasum =
-      if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
-      else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
-
-    val store_heap =
-      build_context.build_heap || Sessions.is_pure(session_name) ||
-      state.sessions.iterator.exists(_.ancestors.contains(session_name))
-
+    val input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum))
+    val store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
     val (current, output_shasum) =
       store.check_output(_database_server, session_name,
-        session_options = build_context.sessions_structure(session_name).options,
         sources_shasum = sources_shasum,
         input_shasum = input_shasum,
+        build_thorough = build_context.sessions_structure(session_name).build_thorough,
         fresh_build = build_context.fresh_build,
         store_heap = store_heap)
 
@@ -1302,7 +1298,7 @@
       finished || sleep
     }
 
-  protected def init_unsynchronized(): Unit = {
+  protected def init_unsynchronized(): Unit =
     if (build_context.master) {
       val sessions1 =
         _state.sessions.init(build_context, _database_server, progress = build_progress)
@@ -1315,10 +1311,6 @@
       _state = _state.copy(sessions = sessions1, pending = pending1)
     }
 
-    val numa_nodes = Host.numa_nodes(enabled = build_context.numa_shuffling)
-    _state = _state.copy(numa_nodes = numa_nodes)
-  }
-
   protected def main_unsynchronized(): Unit = {
     for (job <- _state.running.valuesIterator; build <- job.build if build.is_finished) {
       val result = build.join
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -471,8 +471,9 @@
 
       if (used.length >= host.max_jobs) false
       else {
-        if (host.numa_nodes.length <= 1)
+        if (host.numa_nodes.length <= 1) {
           used.map(host_infos.num_threads).sum + threads <= host.max_threads
+        }
         else {
           def node_threads(n: Int): Int =
             used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum
@@ -1117,23 +1118,13 @@
     def is_current(state: Build_Process.State, session_name: String): Boolean =
       state.ancestor_results(session_name) match {
         case Some(ancestor_results) if ancestor_results.forall(_.current) =>
-          val sources_shasum = state.sessions(session_name).sources_shasum
-
-          val input_shasum =
-            if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
-            else SHA1.flat_shasum(ancestor_results.map(_.output_shasum))
-
-          val store_heap =
-            build_context.build_heap || Sessions.is_pure(session_name) ||
-              state.sessions.iterator.exists(_.ancestors.contains(session_name))
-
           store.check_output(
             _database_server, session_name,
-            session_options = build_context.sessions_structure(session_name).options,
-            sources_shasum = sources_shasum,
-            input_shasum = input_shasum,
+            sources_shasum = state.sessions(session_name).sources_shasum,
+            input_shasum = ML_Process.make_shasum(ancestor_results.map(_.output_shasum)),
+            build_thorough = build_context.sessions_structure(session_name).build_thorough,
             fresh_build = build_context.fresh_build,
-            store_heap = store_heap)._1
+            store_heap = build_context.store_heap || state.sessions.store_heap(session_name))._1
         case _ => false
       }
 
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/sessions.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -577,8 +577,8 @@
     }
   }
 
-  def eq_sources(options: Options, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean =
-    if (options.bool("build_thorough")) shasum1 == shasum2
+  def eq_sources(thorough: Boolean, shasum1: SHA1.Shasum, shasum2: SHA1.Shasum): Boolean =
+    if (thorough) shasum1 == shasum2
     else {
       def trim(shasum: SHA1.Shasum): SHA1.Shasum =
         shasum.filter(s => !is_build_prefs(s))
@@ -721,6 +721,8 @@
     def main_group: Boolean = groups.contains("main")
     def doc_group: Boolean = groups.contains("doc")
 
+    def build_thorough: Boolean = options.bool("build_thorough")
+
     def timeout_ignored: Boolean =
       !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
 
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Build/store.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -83,7 +83,7 @@
       new Sources(
         session_base.session_sources.foldLeft(Map.empty) {
           case (sources, (path, digest)) =>
-            def err(): Nothing = error("Incoherent digest for source file: " + path)
+            def err(): Nothing = error("Incoherent digest for source file: " + path.expand)
             val name = File.symbolic_path(path)
             sources.get(name) match {
               case Some(source_file) =>
@@ -383,7 +383,30 @@
     server: SSH.Server = SSH.no_server
   ): Option[SQL.Database] = {
     if (database_server.isDefined) None
-    else store.maybe_open_database_server(server = server, guard = build_cluster)
+    else maybe_open_database_server(server = server, guard = build_cluster)
+  }
+
+  def maybe_using_heaps_database[A](
+    database_server: Option[SQL.Database],
+    server: SSH.Server = SSH.no_server
+  )(f: SQL.Database => A): Option[A] = {
+    using_optional(maybe_open_heaps_database(database_server, server = server)) {
+      heaps_database => (database_server orElse heaps_database).map(f)
+    }
+  }
+
+  def in_heaps_database(
+    sessions: List[Store.Session],
+    database_server: Option[SQL.Database],
+    server: SSH.Server = SSH.no_server,
+    progress: Progress = new Progress
+  ): Unit = {
+    if (sessions.nonEmpty) {
+      maybe_using_heaps_database(database_server, server = server) { db =>
+        val slice = Space.MiB(options.real("build_database_slice"))
+        sessions.foreach(ML_Heap.store(db, _, slice, cache = cache.compress, progress = progress))
+      }
+    }
   }
 
   def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database =
@@ -462,11 +485,11 @@
   def check_output(
     database_server: Option[SQL.Database],
     name: String,
-    session_options: Options,
     sources_shasum: SHA1.Shasum,
     input_shasum: SHA1.Shasum,
-    fresh_build: Boolean,
-    store_heap: Boolean
+    build_thorough: Boolean = false,
+    fresh_build: Boolean = false,
+    store_heap: Boolean = false
   ): (Boolean, SHA1.Shasum) = {
     def no_check: (Boolean, SHA1.Shasum) = (false, SHA1.no_shasum)
 
@@ -477,7 +500,7 @@
           val current =
             !fresh_build &&
               build.ok &&
-              Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
+              Sessions.eq_sources(build_thorough, build.sources, sources_shasum) &&
               build.input_heaps == input_shasum &&
               build.output_heap == output_shasum &&
               !(store_heap && output_shasum.is_empty)
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -11,16 +11,14 @@
   /** heap file with SHA1 digest **/
 
   private val sha1_prefix = "SHA1:"
+  private val sha1_length = sha1_prefix.length + SHA1.digest_length
 
   def read_file_digest(heap: Path): Option[SHA1.Digest] = {
     if (heap.is_file) {
-      val l = sha1_prefix.length
-      val m = l + SHA1.digest_length
-      val n = File.size(heap)
-      val bs = Bytes.read_file(heap, offset = n - m)
-      if (bs.length == m) {
+      val bs = Bytes.read_file(heap, offset = File.size(heap) - sha1_length)
+      if (bs.length == sha1_length) {
         val s = bs.text
-        if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l)))
+        if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(sha1_prefix.length)))
         else None
       }
       else None
@@ -204,7 +202,7 @@
     val heap_digest = session.heap.map(write_file_digest)
     val heap_size =
       session.heap match {
-        case Some(heap) => File.size(heap) - sha1_prefix.length - SHA1.digest_length
+        case Some(heap) => File.size(heap) - sha1_length
         case None => 0L
       }
 
@@ -285,16 +283,13 @@
 
             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)
+              tmp.file.delete()
               for (slice <- private_data.read_slices(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 " + heap)
+              if (db_digest.get == digest) Isabelle_System.move_file(tmp, heap)
+              else error("Incoherent content for session heap " + heap.expand)
             }
           }
         }
@@ -303,14 +298,14 @@
         /* log_db */
 
         for (session <- sessions; path <- session.log_db) {
-          val file_uuid = Store.read_build_uuid(path, session.name)
-          private_data.read_log_db(db, session.name, old_uuid = file_uuid) match {
-            case Some(log_db) if file_uuid.isEmpty =>
+          val old_uuid = Store.read_build_uuid(path, session.name)
+          for (log_db <- private_data.read_log_db(db, session.name, old_uuid = old_uuid)) {
+            if (old_uuid.isEmpty) {
               progress.echo("Restoring " + session.log_db_name + " ...")
               Isabelle_System.make_directory(path.expand.dir)
               Bytes.write(path, log_db.content)
-            case Some(_) => error("Incoherent content for session database " + path)
-            case None =>
+            }
+            else error("Incoherent content for session database " + path.expand)
           }
         }
       }
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/ML/ml_process.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -12,8 +12,9 @@
 
 
 object ML_Process {
-  def bootstrap_shasum(): SHA1.Shasum =
-    SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+  def make_shasum(ancestors: List[SHA1.Shasum]): SHA1.Shasum =
+    if (ancestors.isEmpty) SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+    else SHA1.flat_shasum(ancestors)
 
   def session_heaps(
     store: Store,
diff -r 601ff5c7cad5 -r 8262d4f63b58 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Wed Apr 17 22:07:07 2024 +0100
+++ b/src/Pure/Tools/update.scala	Wed Apr 17 22:07:21 2024 +0100
@@ -217,13 +217,13 @@
                 sessions = sessions),
               base_logics = base_logics,
               progress = progress,
-              build_heap,
-              clean_build,
+              build_heap = build_heap,
+              clean_build = clean_build,
               dirs = dirs,
               select_dirs = select_dirs,
               numa_shuffling = Host.numa_check(progress, numa_shuffling),
               max_jobs = max_jobs,
-              fresh_build,
+              fresh_build = fresh_build,
               no_build = no_build)
           }