# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700664418 -3600
# Node ID 1c91e884035d9b48c3976eb4e82ce4e0f1da3e88
# Parent  ef76705bf40205c8fee39b6e3eb167d3af0063e7
properly incorporate running tasks into timing heuristic;

diff -r ef76705bf402 -r 1c91e884035d src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Wed Nov 22 15:39:39 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Wed Nov 22 15:46:58 2023 +0100
@@ -429,15 +429,16 @@
       val ordered_hosts =
         host_infos.hosts.sorted(host_infos.host_speeds).reverse.map(_ -> max_threads)
 
-      val fully_parallelizable =
-        parallel_paths(state.next_ready.map(_.name).toSet) <= resources.unused_nodes(max_threads).length
+      val resources0 = host_infos.available(state.copy(running = Map.empty))
+      val max_parallel = parallel_paths(state.ready.map(_.name).toSet)
+      val fully_parallelizable = max_parallel <= resources0.unused_nodes(max_threads).length
 
       if (fully_parallelizable) {
         val all_tasks = state.next_ready.map(task => (task, best_threads(task), best_threads(task)))
         resources.try_allocate_tasks(ordered_hosts, all_tasks)._1
       }
       else {
-        val critical_nodes = state.next_ready.toSet.flatMap(task => critical_path_nodes(task.name))
+        val critical_nodes = state.ready.toSet.flatMap(task => critical_path_nodes(task.name))
 
         val (critical, other) =
           state.next_ready.sortBy(task => remaining_time_ms(task.name)).reverse.partition(task =>
@@ -446,8 +447,9 @@
         val critical_tasks = critical.map(task => (task, best_threads(task), best_threads(task)))
         val other_tasks = other.map(task => (task, 1, best_threads(task)))
 
-        val (critical_hosts, other_hosts) =
-          ordered_hosts.splitAt(parallel_paths(critical.map(_.name).toSet, critical_nodes.contains))
+        val critical_minimals = critical_nodes.intersect(state.ready.map(_.name).toSet)
+        val max_critical_parallel = parallel_paths(critical_minimals, critical_nodes.contains)
+        val (critical_hosts, other_hosts) = ordered_hosts.splitAt(max_critical_parallel)
 
         val (configs1, resources1) = resources.try_allocate_tasks(critical_hosts, critical_tasks)
         val (configs2, _) = resources1.try_allocate_tasks(other_hosts, other_tasks)