# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1699541151 -3600
# Node ID 26841d3c568c750c6dc4f24e205c20cecd01915d
# Parent  f72f576fea3ea9ed21ee5bf308f176ca42550e5f
performance tuning for build schedule: explicit schedule generation, without mixing heuristics;

diff -r f72f576fea3e -r 26841d3c568c src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Thu Nov 09 11:49:08 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Thu Nov 09 15:45:51 2023 +0100
@@ -306,12 +306,16 @@
     def finished: Boolean = build_state.pending.isEmpty && build_state.running.isEmpty
   }
 
-  abstract class Scheduler(timing_data: Timing_Data) {
+  abstract class Scheduler {
     def ready_jobs(state: Build_Process.State): Build_Process.State.Pending =
       state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name))
 
     def next(state: Build_Process.State): List[Config]
 
+    def build_duration(build_state: Build_Process.State): Time
+  }
+
+  abstract class Heuristic(timing_data: Timing_Data) extends Scheduler {
     def build_duration(build_state: Build_Process.State): Time = {
       @tailrec
       def simulate(state: State): State =
@@ -327,6 +331,17 @@
     }
   }
 
+  class Meta_Heuristic(heuristics: List[Heuristic]) extends Scheduler {
+    require(heuristics.nonEmpty)
+
+    def best_result(state: Build_Process.State): (Heuristic, Time) =
+      heuristics.map(heuristic => heuristic -> heuristic.build_duration(state)).minBy(_._2.ms)
+
+    def next(state: Build_Process.State): List[Config] = best_result(state)._1.next(state)
+
+    def build_duration(state: Build_Process.State): Time = best_result(state)._2
+  }
+
 
   /* heuristics */
 
@@ -334,7 +349,7 @@
     threshold: Time,
     timing_data: Timing_Data,
     sessions_structure: Sessions.Structure
-  ) extends Scheduler(timing_data) {
+  ) extends Heuristic(timing_data) {
     /* pre-computed properties for efficient heuristic */
 
     type Node = String
@@ -409,16 +424,6 @@
     }
   }
 
-  class Meta_Heuristic(schedulers: List[Scheduler], timing_data: Timing_Data)
-    extends Scheduler(timing_data) {
-    require(schedulers.nonEmpty)
-
-    def next(state: Build_Process.State): List[Config] = {
-      val (best, _) = schedulers.map(h => h -> h.build_duration(state)).minBy(_._2.ms)
-      best.next(state)
-    }
-  }
-
 
   /* process for scheduled build */
 
@@ -592,7 +597,7 @@
                 Time.minutes(minutes),
                 timing_data,
                 context.build_deps.sessions_structure))
-          new Meta_Heuristic(heuristics, timing_data)
+          new Meta_Heuristic(heuristics)
         }
       }
   }