only start jobs early if they are due (cf. 1966578feff8);
--- 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] = {