# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1703008292 -3600
# Node ID 123651f3ec5d9ea0d8d72c769679d5f3f89572cb
# Parent  ae0a2cb42b05f252cb1596a409d7ef5c7e45ab41
restore benchmark requirement heaps properly;

diff -r ae0a2cb42b05 -r 123651f3ec5d src/Pure/System/benchmark.scala
--- a/src/Pure/System/benchmark.scala	Tue Dec 19 18:31:05 2023 +0100
+++ b/src/Pure/System/benchmark.scala	Tue Dec 19 18:51:32 2023 +0100
@@ -39,8 +39,6 @@
       using_optional(store.maybe_open_database_server(server = server)) { database_server =>
         val db = store.open_build_database(path = Host.private_data.database, server = server)
 
-        benchmark_requirements(options, progress)
-
         progress.echo("Starting benchmark...")
         val selection = Sessions.Selection(sessions = List(benchmark_session))
         val full_sessions = Sessions.load_structure(options.int("threads") = 1)
@@ -55,6 +53,14 @@
         val heaps = session.ancestors.map(store.output_heap)
         ML_Heap.restore(database_server, heaps, cache = store.cache.compress)
 
+        val local_options =
+          options
+            .bool.update("build_database_server", false)
+            .bool.update("build_database", false)
+
+        benchmark_requirements(local_options, progress)
+        ML_Heap.restore(database_server, heaps, cache = store.cache.compress)
+
         def get_shasum(session_name: String): SHA1.Shasum = {
           val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
 
@@ -76,8 +82,7 @@
         val input_shasum = get_shasum(benchmark_session)
         val node_info = Host.Node_Info(hostname, None, Nil)
 
-        val local_build_context =
-          build_context.copy(store = Store(options.bool("build_database_server") = false))
+        val local_build_context = build_context.copy(store = Store(local_options))
 
         val build =
           Build_Job.start_session(local_build_context, session, progress, No_Logger, server,