# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1702052201 -3600
# Node ID 5db03f9276e20131e0bdfd4e80d7f71217e7a8b9
# Parent  ee405c40db72478235b973411ba7e858b22af88b
clarified: build schedules may be outdated when empty, after some time, or due to build progress;

diff -r ee405c40db72 -r 5db03f9276e2 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 08 17:00:13 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 08 17:16:41 2023 +0100
@@ -455,10 +455,12 @@
     def duration: Time = end.time - start.time
     def message: String = "Estimated " + duration.message_hms + " build time with " + generator
 
-    def is_current(state: Build_Process.State): Boolean =
-      !graph.is_empty && graph.minimals.toSet.intersect(state.results.keySet).isEmpty
-    def is_current_estimate(other: Schedule): Boolean =
-      (end.time - other.end.time).minutes.abs < 1
+    def deviation(other: Schedule): Time = Time.ms((end.time - other.end.time).ms.abs)
+
+    def num_built(state: Build_Process.State): Int = graph.keys.count(state.results.contains)
+    def elapsed(): Time = Time.now() - start.time
+    def is_outdated(state: Build_Process.State, time_limit: Time, built_limit: Int): Boolean =
+      graph.is_empty || (elapsed() > time_limit && num_built(state) > built_limit)
 
     def next(hostname: String, state: Build_Process.State): List[String] =
       for {
@@ -945,8 +947,9 @@
         case _ => false
     }
 
-    override def next_jobs(state: Build_Process.State): List[String] = {
-      if (!progress.stopped && _schedule.is_current(state)) _schedule.next(hostname, state)
+    override def next_jobs(state: Build_Process.State): List[String] =
+      if (!progress.stopped && !_schedule.is_outdated(state, Time.minutes(3), 10))
+        _schedule.next(hostname, state)
       else if (!build_context.master) Nil
       else if (progress.stopped) state.next_ready.map(_.name)
       else {
@@ -958,13 +961,12 @@
           val elapsed = Time.now() - start
 
           val timing_msg = if (elapsed.is_relevant) " (took " + elapsed.message + ")" else ""
-          progress.echo_if(!_schedule.is_current_estimate(schedule), schedule.message + timing_msg)
+          progress.echo_if(_schedule.deviation(schedule).minutes > 1, schedule.message + timing_msg)
 
           _schedule = schedule
           _schedule.next(hostname, state)
         }
       }
-    }
 
     override def run(): Build.Results = {
       val results = super.run()