src/Pure/Tools/build_schedule.scala
changeset 79191 ee405c40db72
parent 79190 2039f3609884
child 79192 5db03f9276e2
equal deleted inserted replaced
79190:2039f3609884 79191:ee405c40db72
   462 
   462 
   463     def next(hostname: String, state: Build_Process.State): List[String] =
   463     def next(hostname: String, state: Build_Process.State): List[String] =
   464       for {
   464       for {
   465         task <- state.next_ready
   465         task <- state.next_ready
   466         node = graph.get_node(task.name)
   466         node = graph.get_node(task.name)
   467         if node.start.time == start.time
       
   468         if hostname == node.node_info.hostname
   467         if hostname == node.node_info.hostname
       
   468         if graph.imm_preds(node.job_name).subsetOf(state.results.keySet)
   469       } yield task.name
   469       } yield task.name
   470   }
   470   }
   471 
   471 
   472   case class State(build_state: Build_Process.State, current_time: Time, finished: Schedule) {
   472   case class State(build_state: Build_Process.State, current_time: Time, finished: Schedule) {
   473     def start(config: Config): State =
   473     def start(config: Config): State =
   489       else {
   489       else {
   490         val (job, elapsed) = remaining.minBy(_._2.ms)
   490         val (job, elapsed) = remaining.minBy(_._2.ms)
   491         val now = current_time + elapsed
   491         val now = current_time + elapsed
   492         val node = Schedule.Node(job.name, job.node_info, job.start_date, now - job.start_date.time)
   492         val node = Schedule.Node(job.name, job.node_info, job.start_date, now - job.start_date.time)
   493 
   493 
   494         val preds =
   494         val host_preds =
       
   495           for {
       
   496             (name, (node, _)) <- finished.graph.iterator.toSet
       
   497             if node.node_info.hostname == job.node_info.hostname
       
   498           } yield name
       
   499         val build_preds =
   495           build_state.sessions.graph.imm_preds(job.name).filter(finished.graph.defined)
   500           build_state.sessions.graph.imm_preds(job.name).filter(finished.graph.defined)
   496         val graph =
   501         val preds = build_preds ++ host_preds
   497           preds.foldLeft(finished.graph.new_node(job.name, node))(_.add_edge(_, job.name))
   502 
       
   503         val graph = preds.foldLeft(finished.graph.new_node(job.name, node))(_.add_edge(_, job.name))
   498 
   504 
   499         val build_state1 = build_state.remove_running(job.name).remove_pending(job.name)
   505         val build_state1 = build_state.remove_running(job.name).remove_pending(job.name)
   500         State(build_state1, now, finished.copy(graph = graph))
   506         State(build_state1, now, finished.copy(graph = graph))
   501       }
   507       }
   502     }
   508     }