# HG changeset patch # User wenzelm # Date 1678724563 -3600 # Node ID 86ef80d135447db290601e42780ce6fed2e8e3a1 # Parent 979baa91da0f31c2af8ef67943fe930abee96f10 clarified signature: avoid confusion due to object-orientation; diff -r 979baa91da0f -r 86ef80d13544 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon Mar 13 16:53:08 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Mon Mar 13 17:22:43 2023 +0100 @@ -12,12 +12,10 @@ trait Build_Job { def job_name: String - def worker_uuid: String def node_info: Host.Node_Info def cancel(): Unit = () def is_finished: Boolean = false def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) - def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, worker_uuid, node_info) } object Build_Job { @@ -25,14 +23,6 @@ def ok: Boolean = process_result.ok } - sealed case class Abstract( - override val job_name: String, - override val worker_uuid: String, - override val node_info: Host.Node_Info - ) extends Build_Job { - override def make_abstract: Abstract = this - } - /* build session */ @@ -40,15 +30,13 @@ def start_session( build_context: Build_Process.Context, - worker_uuid: String, progress: Progress, log: Logger, session_background: Sessions.Background, input_shasum: SHA1.Shasum, node_info: Host.Node_Info ): Session_Job = { - new Session_Job( - build_context, worker_uuid, progress, log, session_background, input_shasum, node_info) + new Session_Job(build_context, progress, log, session_background, input_shasum, node_info) } object Session_Context { @@ -114,7 +102,6 @@ class Session_Job private[Build_Job]( build_context: Build_Process.Context, - override val worker_uuid: String, progress: Progress, log: Logger, session_background: Sessions.Background, diff -r 979baa91da0f -r 86ef80d13544 src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Mon Mar 13 16:53:08 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Mon Mar 13 17:22:43 2023 +0100 @@ -149,6 +149,15 @@ if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this } + case class Job( + name: String, + worker_uuid: String, + node_info: Host.Node_Info, + build: Option[Build_Job] + ) { + def no_build: Job = copy(build = None) + } + case class Worker( worker_uuid: String, build_uuid: String, @@ -173,7 +182,7 @@ type Sessions = Map[String, Build_Job.Session_Context] type Workers = List[Worker] type Pending = List[Task] - type Running = Map[String, Build_Job] + type Running = Map[String, Job] type Results = Map[String, Result] def inc_serial(serial: Long): Long = { @@ -229,13 +238,16 @@ def is_running(name: String): Boolean = running.isDefinedAt(name) - def stop_running(): Unit = running.valuesIterator.foreach(_.cancel()) + def stop_running(): Unit = + for (job <- running.valuesIterator; build <- job.build) build.cancel() def finished_running(): List[Build_Job] = - List.from(running.valuesIterator.filter(_.is_finished)) + List.from( + for (job <- running.valuesIterator; build <- job.build if build.is_finished) + yield build) - def add_running(name: String, job: Build_Job): State = - copy(running = running + (name -> job)) + def add_running(job: Job): State = + copy(running = running + (job.name -> job)) def remove_running(name: String): State = copy(running = running - name) @@ -599,34 +611,34 @@ val table = make_table("running", List(name, worker_uuid, hostname, numa_node)) } - def read_running(db: SQL.Database): List[Build_Job.Abstract] = + def read_running(db: SQL.Database): List[Job] = db.execute_query_statement( Running.table.select(sql = SQL.order_by(List(Running.name))), - List.from[Build_Job.Abstract], + List.from[Job], { res => val name = res.string(Running.name) val worker_uuid = res.string(Running.worker_uuid) val hostname = res.string(Running.hostname) val numa_node = res.get_int(Running.numa_node) - Build_Job.Abstract(name, worker_uuid, Host.Node_Info(hostname, numa_node)) + Job(name, worker_uuid, Host.Node_Info(hostname, numa_node), None) } ) def update_running(db: SQL.Database, running: State.Running): Boolean = { - val old_running = read_running(db) - val abs_running = running.valuesIterator.map(_.make_abstract).toList + val running0 = read_running(db) + val running1 = running.valuesIterator.map(_.no_build).toList - val (delete, insert) = Library.symmetric_difference(old_running, abs_running) + val (delete, insert) = Library.symmetric_difference(running0, running1) if (delete.nonEmpty) { db.execute_statement( - Running.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.job_name))))) + Running.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name))))) } for (job <- insert) { db.execute_statement(Running.table.insert(), body = { stmt => - stmt.string(1) = job.job_name + stmt.string(1) = job.name stmt.string(2) = job.worker_uuid stmt.string(3) = job.node_info.hostname stmt.int(4) = job.node_info.numa_node @@ -902,10 +914,11 @@ store.init_output(session_name) - val job = - Build_Job.start_session(build_context, worker_uuid, progress, log, + val build = + Build_Job.start_session(build_context, progress, log, build_deps.background(session_name), input_shasum, node_info) - state1.add_running(session_name, job) + + state1.add_running(Build_Process.Job(session_name, worker_uuid, node_info, Some(build))) } } @@ -982,14 +995,14 @@ while (!finished()) { if (progress.stopped) synchronized_database { _state.stop_running() } - for (job <- synchronized_database { _state.finished_running() }) { - val job_name = job.job_name - val (process_result, output_shasum) = job.join + for (build <- synchronized_database { _state.finished_running() }) { + val job_name = build.job_name + val (process_result, output_shasum) = build.join synchronized_database { _state = _state. remove_pending(job_name). remove_running(job_name). - make_result(job_name, process_result, output_shasum, node_info = job.node_info) + make_result(job_name, process_result, output_shasum, node_info = build.node_info) } }