--- a/src/Pure/Build/build_benchmark.scala Tue Apr 16 16:54:15 2024 +0200
+++ b/src/Pure/Build/build_benchmark.scala Tue Apr 16 17:06:05 2024 +0200
@@ -65,14 +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 input_shasum = ML_Process.make_shasum(sessions(session_name).ancestors.map(get_shasum))
- 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)._2
- }
+ def get_shasum(name: String): SHA1.Shasum =
+ store.check_output(database_server, name,
+ session_options = build_context.sessions_structure(name).options,
+ sources_shasum = sessions(name).sources_shasum,
+ input_shasum = ML_Process.make_shasum(sessions(name).ancestors.map(get_shasum)))._2
val deps = Sessions.deps(full_sessions.selection(selection)).check_errors
val background = deps.background(benchmark_session_name)
--- a/src/Pure/Build/build_schedule.scala Tue Apr 16 16:54:15 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala Tue Apr 16 17:06:05 2024 +0200
@@ -1118,19 +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 = ML_Process.make_shasum(ancestor_results.map(_.output_shasum))
-
- val store_heap = build_context.store_heap || state.sessions.store_heap(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)),
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
}