# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1701460385 -3600
# Node ID f5a2f956b53122fa16f0ccd65f3dd1b1771bca12
# Parent  91955d607aad24f4b6b4b0eee1496eb294cdec7e
add heuristic for non-scheduled (standard) build behaviour;

diff -r 91955d607aad -r f5a2f956b531 src/Pure/Tools/build_schedule.scala
--- a/src/Pure/Tools/build_schedule.scala	Fri Dec 01 20:51:33 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Dec 01 20:53:05 2023 +0100
@@ -491,6 +491,30 @@
     }
   }
 
+  class Default_Heuristic(timing_data: Timing_Data, options: Options)
+    extends Heuristic(timing_data) {
+
+    def host_threads(host: Host): Int = {
+      val m = (options ++ host.build.options).int("threads")
+      if (m > 0) m else (host.num_cpus max 1) min 8
+    }
+    
+    def next_jobs(resources: Resources, sorted_jobs: List[String], host: Host): List[Config] =
+      sorted_jobs.zip(resources.unused_nodes(host, host_threads(host))).map(Config(_, _))
+
+    def next(state: Build_Process.State): List[Config] = {
+      val sorted_jobs = state.next_ready.sortBy(_.name)(state.sessions.ordering).map(_.name)
+      val resources = host_infos.available(state)
+
+      host_infos.hosts.foldLeft((sorted_jobs, List.empty[Config])) {
+        case ((jobs, res), host) =>
+          val configs = next_jobs(resources, jobs, host)
+          val config_jobs = configs.map(_.job_name).toSet
+          (jobs.filterNot(config_jobs.contains), configs ::: res)
+      }._2
+    }
+  }
+
   class Meta_Heuristic(heuristics: List[Heuristic]) extends Scheduler {
     require(heuristics.nonEmpty)