partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded;
authorFabian Huch <huch@in.tum.de>
Mon, 04 Mar 2024 16:20:57 +0100
changeset 79765 a478fc5cd5bd
parent 79764 5857bb16cf30
child 79766 feec445a82c3
partially revert f1f08ca40d96: benchmark data needs to be present before timing data is loaded;
src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Mon Mar 04 13:55:11 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Mon Mar 04 16:20:57 2024 +0100
@@ -915,6 +915,20 @@
 
     /* previous results via build log */
 
+    override def open_build_cluster(): Build_Cluster = {
+      val build_cluster = super.open_build_cluster()
+      build_cluster.init()
+
+      Build_Benchmark.benchmark_requirements(build_options)
+
+      if (build_context.worker) {
+        val benchmark_options = build_options.string("build_hostname") = hostname
+        Build_Benchmark.benchmark(benchmark_options, progress)
+      }
+
+      build_cluster.benchmark()
+    }
+
     private val timing_data: Timing_Data = {
       val cluster_hosts: List[Build_Cluster.Host] =
         if (build_context.jobs == 0) build_context.build_hosts
@@ -1030,14 +1044,6 @@
       }
 
     override def run(): Build.Results = {
-      Build_Benchmark.benchmark_requirements(build_options)
-
-      if (build_context.worker) {
-        val benchmark_options = build_options.string.update("build_hostname", hostname)
-        Build_Benchmark.benchmark(benchmark_options, progress)
-      }
-      _build_cluster.benchmark()
-
       for (db <- _build_database)
         Build_Process.private_data.transaction_lock(db, label = "Scheduler_Build_Process.init") {
           Build_Process.private_data.clean_build(db)