--- a/src/Pure/Build/build.scala Tue Apr 16 14:48:08 2024 +0200
+++ b/src/Pure/Build/build.scala Tue Apr 16 15:11:13 2024 +0200
@@ -36,7 +36,7 @@
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 = (_, _) => (),
@@ -256,7 +256,7 @@
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,
+ 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)
--- a/src/Pure/Build/build_process.scala Tue Apr 16 14:48:08 2024 +0200
+++ b/src/Pure/Build/build_process.scala Tue Apr 16 15:11:13 2024 +0200
@@ -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)
@@ -1165,9 +1168,7 @@
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 store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
val (current, output_shasum) =
store.check_output(_database_server, session_name,
--- a/src/Pure/Build/build_schedule.scala Tue Apr 16 14:48:08 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala Tue Apr 16 15:11:13 2024 +0200
@@ -1124,9 +1124,7 @@
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 store_heap = build_context.store_heap || state.sessions.store_heap(session_name)
store.check_output(
_database_server, session_name,