src/Pure/Build/build_schedule.scala

           (meta_info, build_info) <- build_history
           build_host = meta_info.get_build_host
           (job_name, session_info) <- build_info.sessions.toList
           if build_info.finished_sessions.contains(job_name)
           hostname <- session_info.hostname.orElse(build_host).toList
-          host <- hosts.find(_.info.hostname == hostname).toList
-          threads = session_info.threads.getOrElse(host.info.num_cpus)
+          host <- hosts.find(_.name == hostname).toList
+          threads = session_info.threads.getOrElse(host.num_cpus)
         } yield (job_name, hostname, threads) -> session_info.timing
 
       val entries =
         if (measurements.isEmpty) {
           val default_host = host_infos.hosts.sorted(host_infos.host_speeds).last

   }
 
 
   /* host information */
 
-  case class Host(info: isabelle.Host.Info, build: Build_Cluster.Host) {
-    def name: String = info.hostname
-    def num_cpus: Int = info.num_cpus
-    def max_threads(options: Options): Int = (options ++ build.options).threads(default = num_cpus)
+  case class Host(
+    name: String,
+    num_cpus: Int,
+    max_jobs: Int,
+    benchmark_score: Double,
+    numa: Boolean = false,
+    numa_nodes: List[Int] = Nil,
+    options: List[Options.Spec] = Nil
+  ) {
+    def max_threads(options: Options): Int = (options ++ this.options).threads(default = num_cpus)
   }
 
   object Host_Infos {
     def load(build_hosts: List[Build_Cluster.Host], db: SQL.Database): Host_Infos = {
       def get_host(build_host: Build_Cluster.Host): Host = {
+        val name = build_host.name
         val info =
-          isabelle.Host.read_info(db, build_host.name).getOrElse(
-            error("No benchmark for " + quote(build_host.name)))
-        Host(info, build_host)
+          isabelle.Host.read_info(db, name).getOrElse(error("No info for host " + quote(name)))
+        val score = info.benchmark_score.getOrElse(error("No benchmark for " + quote(name)))
+
+        Host(
+          name = name,
+          num_cpus = info.num_cpus,
+          max_jobs = build_host.jobs,
+          numa = build_host.numa,
+          numa_nodes = info.numa_nodes,
+          benchmark_score = score,
+          options = build_host.options)
       }
 
       new Host_Infos(build_hosts.map(get_host))
     }
   }

     require(hosts.nonEmpty)
 
     private val by_hostname = hosts.map(host => host.name -> host).toMap
 
     def host_factor(from: Host, to: Host): Double =
-      from.info.benchmark_score.get / to.info.benchmark_score.get
+      from.benchmark_score / to.benchmark_score
 
     val host_speeds: Ordering[Host] =
       Ordering.fromLessThan((host1, host2) => host_factor(host1, host2) < 1)
 
     def the_host(hostname: String): Host =
       by_hostname.getOrElse(hostname, error("Unknown host " + quote(hostname)))
     def the_host(node_info: Node_Info): Host = the_host(node_info.hostname)
 
     def num_threads(node_info: Node_Info): Int =
       if (node_info.rel_cpus.nonEmpty) node_info.rel_cpus.length
-      else the_host(node_info).info.num_cpus
+      else the_host(node_info).num_cpus
 
     def available(state: Build_Process.State): Resources = {
       val allocated =
         state.running.values.map(_.node_info).groupMapReduce(_.hostname)(List(_))(_ ::: _)
       new Resources(this, allocated)

         case Nil => (Nil, this)
         case (task, min_threads, max_threads) :: tasks =>
           val (config, resources) =
             hosts.find((host, _) => available(host, min_threads)) match {
               case Some((host, host_max_threads)) =>
-                val free_threads = host.info.num_cpus - ((host.build.jobs - 1) * host_max_threads)
+                val free_threads = host.num_cpus - ((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)
             }
           val (configs, resources1) = resources.try_allocate_tasks(hosts, tasks)
           (configs ++ config, resources1)
       }
 
     def next_node(host: Host, threads: Int): Node_Info = {
-      val numa_node_num_cpus = host.info.num_cpus / (host.info.numa_nodes.length max 1)
+      val numa_node_num_cpus = host.num_cpus / (host.numa_nodes.length max 1)
       def explicit_cpus(node_info: Node_Info): List[Int] =
         if (node_info.rel_cpus.nonEmpty) node_info.rel_cpus else (0 until numa_node_num_cpus).toList
 
       val used_nodes = allocated(host).groupMapReduce(_.numa_node)(explicit_cpus)(_ ::: _)
 
-      val available_nodes = host.info.numa_nodes
+      val available_nodes = host.numa_nodes
       val numa_node =
-        if (!host.build.numa) None
+        if (!host.numa) None
         else available_nodes.sortBy(n => used_nodes.getOrElse(Some(n), Nil).length).headOption
 
       val used_cpus = used_nodes.getOrElse(numa_node, Nil).toSet
       val available_cpus = (0 until numa_node_num_cpus).filterNot(used_cpus.contains).toList
 

     }
 
     def available(host: Host, threads: Int): Boolean = {
       val used = allocated(host)
 
-      if (used.length >= host.build.jobs) false
+      if (used.length >= host.max_jobs) false
       else {
-        if (host.info.numa_nodes.length <= 1)
-          used.map(host_infos.num_threads).sum + threads <= host.info.num_cpus
+        if (host.numa_nodes.length <= 1)
+          used.map(host_infos.num_threads).sum + threads <= host.num_cpus
         else {
           def node_threads(n: Int): Int =
             used.filter(_.numa_node.contains(n)).map(host_infos.num_threads).sum
 
-          host.info.numa_nodes.exists(
-            node_threads(_) + threads <= host.info.num_cpus / host.info.numa_nodes.length)
+          host.numa_nodes.exists(
+            node_threads(_) + threads <= host.num_cpus / host.numa_nodes.length)
         }
       }
     }
   }
 

 
     /* pre-computed properties for efficient heuristic */
     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(_.info.num_cpus).max min max_threads_limit
+    val max_threads: Int = host_infos.hosts.map(_.num_cpus).max min max_threads_limit
 
     type Node = String
     val build_graph: Graph[Node, Sessions.Info] = sessions_structure.build_graph
 
     val minimals: List[Node] = build_graph.minimals

     val best_threads: Map[Node, Int] =
       build_graph.keys.map(node => node -> timing_data.best_threads(node, max_threads)).toMap
 
     def best_time(node: Node): Time = {
       val host = ordered_hosts.last
-      val threads = best_threads(node) min host.info.num_cpus
+      val threads = best_threads(node) min host.num_cpus
       timing_data.estimate(node, host.name, threads)
     }
     val best_times: Map[Node, Time] = build_graph.keys.map(node => node -> best_time(node)).toMap
 
     val succs_max_time_ms: Map[Node, Long] = build_graph.node_height(best_times(_).ms)

           this.host_criterion match {
             case Critical_Nodes => max_critical_hosts
             case Fixed_Fraction(fraction) =>
               ((rev_ordered_hosts.length * fraction).ceil.toInt max 1) min max_critical_hosts
             case Host_Speed(min_factor) =>
-              val best = rev_ordered_hosts.head._1.info.benchmark_score.get
+              val best = rev_ordered_hosts.head._1.benchmark_score
               val num_fast =
-                rev_ordered_hosts.count(_._1.info.benchmark_score.exists(_ >= best * min_factor))
+                rev_ordered_hosts.count(_._1.benchmark_score >= best * min_factor)
               num_fast min max_critical_hosts
           }
 
         val (critical_hosts, other_hosts) = rev_ordered_hosts.splitAt(split)