# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710708958 -3600
# Node ID 4359257218cec65cd53d3e8ea66d8750222b9463
# Parent  dc4a387a6f0296078258aa2ef34f83d89dfdd79b
clarify use of num_threads vs. max_cpus;

diff -r dc4a387a6f02 -r 4359257218ce src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Sun Mar 17 21:04:00 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Sun Mar 17 21:55:58 2024 +0100
@@ -50,7 +50,7 @@
           if build_info.finished_sessions.contains(job_name)
           hostname <- session_info.hostname.orElse(build_host).toList
           host <- hosts.find(_.name == hostname).toList
-          threads = session_info.threads.getOrElse(host.num_cpus)
+          threads = session_info.threads.getOrElse(host.max_threads)
         } yield (job_name, hostname, threads) -> session_info.timing
 
       val entries =
@@ -389,7 +389,7 @@
 
     def num_threads(node_info: Node_Info): Int =
       if (node_info.rel_cpus.nonEmpty) node_info.rel_cpus.length
-      else the_host(node_info).num_cpus
+      else the_host(node_info).max_threads
 
     def available(state: Build_Process.State): Resources = {
       val allocated =
@@ -437,7 +437,7 @@
           val (config, resources) =
             hosts.find((host, _) => available(host, min_threads)) match {
               case Some((host, host_max_threads)) =>
-                val free_threads = host.num_cpus - ((host.max_jobs - 1) * host_max_threads)
+                val free_threads = host.max_threads - ((host.max_jobs - 1) * host_max_threads)
                 val node_info = next_node(host, (min_threads max free_threads) min max_threads)
                 (Some(Config(task.name, node_info)), allocate(node_info))
               case None => (None, this)
@@ -472,7 +472,7 @@
       if (used.length >= host.max_jobs) false
       else {
         if (host.numa_nodes.length <= 1)
-          used.map(host_infos.num_threads).sum + threads <= host.num_cpus
+          used.map(host_infos.num_threads).sum + threads <= host.max_threads
         else {
           def node_threads(n: Int): Int =
             used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum
@@ -776,7 +776,7 @@
     val host_infos: Host_Infos = timing_data.host_infos
     val ordered_hosts: List[Host] = host_infos.hosts.sorted(host_infos.host_speeds)
 
-    val max_threads: Int = host_infos.hosts.map(_.num_cpus).max min max_threads_limit
+    val max_threads: Int = host_infos.hosts.map(_.max_threads).max min max_threads_limit
 
     type Node = String
     val build_graph: Graph[Node, Sessions.Info] = sessions_structure.build_graph
@@ -789,7 +789,7 @@
 
     def best_time(node: Node): Time = {
       val host = ordered_hosts.last
-      val threads = best_threads(node) min host.num_cpus
+      val threads = best_threads(node) min host.max_threads
       timing_data.estimate(node, host.name, threads)
     }
     val best_times: Map[Node, Time] = build_graph.keys.map(node => node -> best_time(node)).toMap