tuned;
authorwenzelm
Tue, 16 Apr 2024 17:06:05 +0200
changeset 80125 761bd2b35217
parent 80124 455ddb251ece
child 80126 b73df63e0f52
tuned;
src/Pure/Build/build_benchmark.scala
src/Pure/Build/build_schedule.scala
--- 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
       }