--- a/src/Pure/Build/build_benchmark.scala Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/Build/build_benchmark.scala Tue Apr 16 16:54:15 2024 +0200
@@ -66,12 +66,7 @@
for (db <- database_server) ML_Heap.restore(db, hierachy, cache = store.cache.compress)
def get_shasum(session_name: String): SHA1.Shasum = {
- val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
-
- val input_shasum =
- if (ancestor_shasums.isEmpty) ML_Process.bootstrap_shasum()
- else SHA1.flat_shasum(ancestor_shasums)
-
+ 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,
--- a/src/Pure/Build/build_process.scala Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/Build/build_process.scala Tue Apr 16 16:54:15 2024 +0200
@@ -1163,13 +1163,8 @@
ancestor_results: List[Build_Process.Result]
): Build_Process.State = {
val sources_shasum = state.sessions(session_name).sources_shasum
-
- val input_shasum =
- if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
- else SHA1.flat_shasum(ancestor_results.map(_.output_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)
-
val (current, output_shasum) =
store.check_output(_database_server, session_name,
session_options = build_context.sessions_structure(session_name).options,
--- a/src/Pure/Build/build_schedule.scala Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala Tue Apr 16 16:54:15 2024 +0200
@@ -1120,9 +1120,7 @@
case Some(ancestor_results) if ancestor_results.forall(_.current) =>
val sources_shasum = state.sessions(session_name).sources_shasum
- val input_shasum =
- if (ancestor_results.isEmpty) ML_Process.bootstrap_shasum()
- else SHA1.flat_shasum(ancestor_results.map(_.output_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)
--- a/src/Pure/ML/ml_process.scala Tue Apr 16 16:38:54 2024 +0200
+++ b/src/Pure/ML/ml_process.scala Tue Apr 16 16:54:15 2024 +0200
@@ -12,8 +12,9 @@
object ML_Process {
- def bootstrap_shasum(): SHA1.Shasum =
- SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+ def make_shasum(ancestors: List[SHA1.Shasum]): SHA1.Shasum =
+ if (ancestors.isEmpty) SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE")))
+ else SHA1.flat_shasum(ancestors)
def session_heaps(
store: Store,