# HG changeset patch # User wenzelm # Date 1713279965 -7200 # Node ID 761bd2b352173961509f0531c20c01bdfd1415fc # Parent 455ddb251ece5cbb780a063238025029d70b01a1 tuned; diff -r 455ddb251ece -r 761bd2b35217 src/Pure/Build/build_benchmark.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) diff -r 455ddb251ece -r 761bd2b35217 src/Pure/Build/build_schedule.scala --- 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 }