--- a/src/Pure/Tools/build_job.scala Thu Mar 02 11:36:10 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Thu Mar 02 13:19:21 2023 +0100
@@ -97,9 +97,6 @@
class Session_Job(
build_context: Build_Process.Context,
session_background: Sessions.Background,
- session_heaps: List[Path],
- store_heap: Boolean,
- resources: Resources,
input_shasum: SHA1.Shasum,
override val node_info: Node_Info
) extends Build_Job {
@@ -116,12 +113,20 @@
val session_sources: Sessions.Sources =
Sessions.Sources.load(session_background.base, cache = store.cache.compress)
+ val store_heap = build_context.store_heap(session_name)
+
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
val env =
Isabelle_System.settings(
List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString))
+ val session_heaps =
+ session_background.info.parent match {
+ case None => Nil
+ case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
+ }
+
val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil
val eval_store =
@@ -152,6 +157,10 @@
}
}
+ val resources =
+ new Resources(session_background, log = build_context.log,
+ command_timings = build_context.old_command_timings(session_name))
+
val session =
new Session(options, resources) {
override val cache: Term.Cache = store.cache
--- a/src/Pure/Tools/build_process.scala Thu Mar 02 11:36:10 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Thu Mar 02 13:19:21 2023 +0100
@@ -598,22 +598,11 @@
store.init_output(session_name)
- val session_background = build_deps.background(session_name)
- val session_heaps =
- session_background.info.parent match {
- case None => Nil
- case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic)
- }
-
- val resources =
- new Resources(session_background, log = build_context.log,
- command_timings = build_context.old_command_timings(session_name))
-
val (numa_node, state1) = state.numa_next(build_context.numa_nodes)
val node_info = Build_Job.Node_Info(build_context.hostname, numa_node)
val job =
- new Build_Job.Session_Job(build_context, session_background, session_heaps,
- store_heap, resources, input_shasum, node_info)
+ new Build_Job.Session_Job(
+ build_context, build_deps.background(session_name), input_shasum, node_info)
state1.add_running(session_name, job)
}
}