# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710582989 -3600
# Node ID fbfa7d25749aeb404d25ce56ce5da0505e81a5c3
# Parent  18969501a13e4f736dcba414bf49efaee26dd581
tie-breaking in schedule optimization to pick best schedule even when run-time is dominated by large task (e.g., session with long timeout but no data yet);

diff -r 18969501a13e -r fbfa7d25749a src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sat Mar 16 10:03:10 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sat Mar 16 10:56:29 2024 +0100
@@ -9,6 +9,7 @@
 import Host.Node_Info
 import scala.annotation.tailrec
 import scala.collection.mutable
+import scala.Ordering.Implicits.seqOrdering
 
 
 object Build_Schedule {
@@ -505,6 +506,7 @@
       else graph.maximals.map(graph.get_node).map(_.end).max(Date.Ordering)
 
     def duration: Time = end - start
+    def durations: List[Time] = graph.keys.map(graph.get_node(_).end - start)
     def message: String = "Estimated " + duration.message_hms + " build time with " + generator
 
     def deviation(other: Schedule): Time = Time.ms((end - other.end).ms.abs)
@@ -527,7 +529,7 @@
         if graph.imm_preds(node.job_name).subsetOf(state.results.keySet)
       } yield task.name
 
-    def exists_next(hostname: String, state: Build_Process.State): Boolean = 
+    def exists_next(hostname: String, state: Build_Process.State): Boolean =
       next(hostname, state).nonEmpty
     
     def update(state: Build_Process.State): Schedule = {
@@ -632,7 +634,7 @@
 
     def schedule(state: Build_Process.State): Schedule = {
       def main(scheduler: Scheduler): Schedule = scheduler.schedule(state)
-      Par_List.map(main, schedulers).minBy(_.duration.ms)
+      Par_List.map(main, schedulers).minBy(_.durations.map(_.ms).sorted.reverse)
     }
   }