only start jobs early if they are due (cf. 1966578feff8);
authorFabian Huch <huch@in.tum.de>
Wed, 20 Mar 2024 14:56:16 +0100
changeset 79946 05e034a54924
parent 79945 ca004ccf2352
child 79947 5eb90c1ce653
only start jobs early if they are due (cf. 1966578feff8);
src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Mar 21 14:19:39 2024 +0000
+++ b/src/Pure/Build/build_schedule.scala	Wed Mar 20 14:56:16 2024 +0100
@@ -573,6 +573,8 @@
       else elapsed() > options.seconds("build_schedule_outdated_delay")
 
     def next(hostname: String, state: Build_Process.State): List[String] = {
+      val now = Time.now()
+
       val next_nodes =
         for {
           task <- state.next_ready
@@ -581,8 +583,10 @@
           if hostname == node.node_info.hostname
         } yield node
 
-      val (ready, waiting) =
+      val (ready, other) =
         next_nodes.partition(node => graph.imm_preds(node.job_name).subsetOf(state.results.keySet))
+
+      val waiting = other.filter(_.start.time <= now)
       val running = state.running.values.toList.map(_.node_info).filter(_.hostname == hostname)
 
       def try_run(ready: List[Schedule.Node], next: Schedule.Node): List[Schedule.Node] = {