# HG changeset patch # User Fabian Huch # Date 1718028173 -7200 # Node ID 02f8a35ed8e2a8dd5ae2a859a8c7748c1c500be3 # Parent e070eca8c7314b0c44b8400b58f8c12e9e3c1d0a clarified names: more canonical; diff -r e070eca8c731 -r 02f8a35ed8e2 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Mon Jun 10 15:13:21 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Mon Jun 10 16:02:53 2024 +0200 @@ -99,12 +99,12 @@ sealed case class Task( build_config: Build_Config, hosts_spec: String, - id: UUID.T = UUID.random(), + uuid: UUID.T = UUID.random(), submit_date: Date = Date.now(), priority: Priority = Priority.normal, isabelle_rev: String = "" ) extends T { - def name: String = id.toString + def name: String = uuid.toString def kind: String = build_config.name def components: List[Component] = build_config.components @@ -114,16 +114,16 @@ } sealed case class Job( - id: UUID.T, + uuid: UUID.T, kind: String, - number: Long, + id: Long, isabelle_rev: String, build_cluster: Boolean, hostnames: List[String], components: List[Component], start_date: Date = Date.now(), cancelled: Boolean = false - ) extends T { def name: String = kind + "/" + number } + ) extends T { def name: String = kind + "/" + id } object Status { def from_result(result: Process_Result): Status = { @@ -137,12 +137,12 @@ sealed case class Result( kind: String, - number: Long, + id: Long, status: Status, - id: Option[UUID.T] = None, + uuid: Option[UUID.T] = None, date: Date = Date.now(), serial: Long = 0, - ) extends T { def name: String = kind + "/" + number } + ) extends T { def name: String = kind + "/" + id } object State { def max_serial(serials: Iterable[Long]): Long = serials.maxOption.getOrElse(0L) @@ -196,8 +196,8 @@ running.values.map(_.kind) ++ finished.values.map(_.kind)).toList.distinct - def next_number(kind: String): Long = { - val serials = get_finished(kind).map(_.number) ::: get_running(kind).map(_.number) + def next_id(kind: String): Long = { + val serials = get_finished(kind).map(_.id) ::: get_running(kind).map(_.id) State.inc_serial(State.max_serial(serials)) } @@ -210,10 +210,10 @@ def get(name: String): Option[T] = pending.get(name).orElse(running.get(name)).orElse(finished.get(name)) - def get(id: UUID.T): Option[T] = - pending.values.find(_.id == id).orElse( - running.values.find(_.id == id)).orElse( - finished.values.find(_.id.contains(id))) + def get(uuid: UUID.T): Option[T] = + pending.values.find(_.uuid == uuid).orElse( + running.values.find(_.uuid == uuid)).orElse( + finished.values.find(_.uuid.contains(uuid))) } @@ -280,7 +280,7 @@ val kind = SQL.Column.string("kind") val build_cluster = SQL.Column.bool("build_cluster") val hosts_spec = SQL.Column.string("hosts_spec") - val id = SQL.Column.string("id").make_primary_key + val uuid = SQL.Column.string("uuid").make_primary_key val submit_date = SQL.Column.date("submit_date") val priority = SQL.Column.string("priority") val isabelle_rev = SQL.Column.string("isabelle_rev") @@ -302,7 +302,7 @@ val verbose = SQL.Column.bool("verbose") val table = - make_table(List(kind, build_cluster, hosts_spec, id, submit_date, priority, isabelle_rev, + make_table(List(kind, build_cluster, hosts_spec, uuid, submit_date, priority, isabelle_rev, components, prefs, requirements, all_sessions, base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions, build_heap, clean_build, export_files, fresh_build, presentation, verbose), @@ -315,7 +315,7 @@ val kind = res.string(Pending.kind) val build_cluster = res.bool(Pending.build_cluster) val hosts_spec = res.string(Pending.hosts_spec) - val id = res.string(Pending.id) + val uuid = res.string(Pending.uuid) val submit_date = res.date(Pending.submit_date) val priority = Priority.valueOf(res.string(Pending.priority)) val isabelle_rev = res.string(Pending.isabelle_rev) @@ -347,7 +347,7 @@ } val task = - Task(build_config, hosts_spec, UUID.make(id), submit_date, priority, isabelle_rev) + Task(build_config, hosts_spec, UUID.make(uuid), submit_date, priority, isabelle_rev) task.name -> task }) @@ -358,10 +358,10 @@ pending: Build_Manager.State.Pending ): Update = { val update = Update.make(old_pending, pending) - val delete = update.delete.map(old_pending(_).id.toString) + val delete = update.delete.map(old_pending(_).uuid.toString) if (update.deletes) - db.execute_statement(Pending.table.delete(Pending.id.where_member(delete))) + db.execute_statement(Pending.table.delete(Pending.uuid.where_member(delete))) if (update.inserts) { db.execute_batch_statement(Pending.table.insert(), batch = @@ -370,7 +370,7 @@ stmt.string(1) = task.kind stmt.bool(2) = task.build_cluster stmt.string(3) = task.hosts_spec - stmt.string(4) = task.id.toString + stmt.string(4) = task.uuid.toString stmt.date(5) = task.submit_date stmt.string(6) = task.priority.toString stmt.string(7) = task.isabelle_rev @@ -406,9 +406,9 @@ /* running */ object Running { - val id = SQL.Column.string("id").make_primary_key + val uuid = SQL.Column.string("uuid").make_primary_key val kind = SQL.Column.string("kind") - val number = SQL.Column.long("number") + val id = SQL.Column.long("id") val isabelle_rev = SQL.Column.string("isabelle_rev") val build_cluster = SQL.Column.bool("build_cluster") val hostnames = SQL.Column.string("hostnames") @@ -417,7 +417,7 @@ val cancelled = SQL.Column.bool("cancelled") val table = - make_table(List(id, kind, number, isabelle_rev, build_cluster, hostnames, components, + make_table(List(uuid, kind, id, isabelle_rev, build_cluster, hostnames, components, start_date, cancelled), name = "running") } @@ -425,9 +425,9 @@ def pull_running(db: SQL.Database): Build_Manager.State.Running = db.execute_query_statement(Running.table.select(), Map.from[String, Job], get = { res => - val id = res.string(Running.id) + val uuid = res.string(Running.uuid) val kind = res.string(Running.kind) - val number = res.long(Running.number) + val id = res.long(Running.id) val isabelle_rev = res.string(Running.isabelle_rev) val build_cluster = res.bool(Running.build_cluster) val hostnames = space_explode(',', res.string(Running.hostnames)) @@ -435,7 +435,7 @@ val start_date = res.date(Running.start_date) val cancelled = res.bool(Running.cancelled) - val job = Job(UUID.make(id), kind, number, isabelle_rev, build_cluster, hostnames, + val job = Job(UUID.make(uuid), kind, id, isabelle_rev, build_cluster, hostnames, components, start_date, cancelled) job.name -> job @@ -447,18 +447,18 @@ running: Build_Manager.State.Running ): Update = { val update = Update.make(old_running, running) - val delete = update.delete.map(old_running(_).id.toString) + val delete = update.delete.map(old_running(_).uuid.toString) if (update.deletes) - db.execute_statement(Running.table.delete(Running.id.where_member(delete))) + db.execute_statement(Running.table.delete(Running.uuid.where_member(delete))) if (update.inserts) { db.execute_batch_statement(Running.table.insert(), batch = for (name <- update.insert) yield { (stmt: SQL.Statement) => val job = running(name) - stmt.string(1) = job.id.toString + stmt.string(1) = job.uuid.toString stmt.string(2) = job.kind - stmt.long(3) = job.number + stmt.long(3) = job.id stmt.string(4) = job.isabelle_rev stmt.bool(5) = job.build_cluster stmt.string(6) = job.hostnames.mkString(",") @@ -475,13 +475,13 @@ object Finished { val kind = SQL.Column.string("kind") - val number = SQL.Column.long("number") + val id = SQL.Column.long("id") val status = SQL.Column.string("status") - val id = SQL.Column.string("id") + val uuid = SQL.Column.string("uuid") val date = SQL.Column.date("date") val serial = SQL.Column.long("serial").make_primary_key - val table = make_table(List(kind, number, status, id, date, serial), name = "finished") + val table = make_table(List(kind, id, status, uuid, date, serial), name = "finished") } def read_finished_serial(db: SQL.Database): Long = @@ -501,13 +501,13 @@ Map.from[String, Result], get = { res => val kind = res.string(Finished.kind) - val number = res.long(Finished.number) + val id = res.long(Finished.id) val status = Status.valueOf(res.string(Finished.status)) - val id = res.get_string(Finished.id).map(UUID.make) + val uuid = res.get_string(Finished.uuid).map(UUID.make) val date = res.date(Finished.date) val serial = res.long(Finished.serial) - val result = Result(kind, number, status, id, date, serial) + val result = Result(kind, id, status, uuid, date, serial) result.name -> result } ) @@ -527,9 +527,9 @@ db.execute_batch_statement(Finished.table.insert(), batch = for (result <- insert) yield { (stmt: SQL.Statement) => stmt.string(1) = result.kind - stmt.long(2) = result.number + stmt.long(2) = result.id stmt.string(3) = result.status.toString - stmt.string(4) = result.id.map(_.toString) + stmt.string(4) = result.uuid.map(_.toString) stmt.date(5) = result.date stmt.long(6) = result.serial }) @@ -678,8 +678,8 @@ _state = _state.remove_pending(task.name) - val number = _state.next_number(task.kind) - val context = Context(store, task, number) + val id = _state.next_id(task.kind) + val context = Context(store, task, id) Exn.capture { context.init() @@ -701,18 +701,18 @@ else error("Unknown component " + component) } - Job(task.id, task.kind, number, isabelle_rev, task.build_cluster, hostnames, components) + Job(task.uuid, task.kind, id, isabelle_rev, task.build_cluster, hostnames, components) } match { case Exn.Res(job) => _state = _state.add_running(job) val msg = "Starting " + job.name - echo(msg + " (id " + job.id + ")") + echo(msg + " (id " + job.uuid + ")") context.progress.echo(msg) Some(context) case Exn.Exn(exn) => - val result = Result(task.kind, number, Status.aborted) + val result = Result(task.kind, id, Status.aborted) _state = _state.add_finished(result) val msg = "Failed to start job: " + exn.getMessage @@ -735,11 +735,11 @@ private def finish_job(name: String, process_result: Process_Result): Unit = synchronized_database("finish_job") { val job = _state.running(name) - val result = Result(job.kind, job.number, Status.from_result(process_result), Some(job.id)) + val result = Result(job.kind, job.id, Status.from_result(process_result), Some(job.uuid)) val interrupted_error = process_result.interrupted && process_result.err.nonEmpty val err_msg = if_proper(interrupted_error, ": " + process_result.err) - echo("Finished job " + job.id + " with status code " + process_result.rc + err_msg) + echo("Finished job " + job.uuid + " with status code " + process_result.rc + err_msg) _state = _state .remove_running(job.name) @@ -925,8 +925,8 @@ def link_kind(kind: String): XML.Elem = frontend_link(paths.frontend_url(Page.OVERVIEW, Markup.Kind(kind)), text(kind)) - def link_build(name: String, number: Long): XML.Elem = - frontend_link(paths.frontend_url(Page.BUILD, Markup.Name(name)), text("#" + number)) + def link_build(name: String, id: Long): XML.Elem = + frontend_link(paths.frontend_url(Page.BUILD, Markup.Name(name)), text("#" + id)) private def render_page(name: String)(body: => XML.Body): XML.Body = { def nav_link(path: Path, s: String): XML.Elem = @@ -938,32 +938,32 @@ def render_home(state: State): XML.Body = render_page("Dashboard") { def render_kind(kind: String): XML.Elem = { - val running = state.get_running(kind).sortBy(_.number).reverse - val finished = state.get_finished(kind).sortBy(_.number).reverse + val running = state.get_running(kind).sortBy(_.id).reverse + val finished = state.get_finished(kind).sortBy(_.id).reverse def render_previous(finished: List[Result]): XML.Body = { val (failed, rest) = finished.span(_.status != Status.ok) val first_failed = failed.lastOption.map(result => par( text("first failure: ") ::: - link_build(result.name, result.number) :: + link_build(result.name, result.id) :: text(" on " + result.date))) val last_success = rest.headOption.map(result => par( - text("last success: ") ::: link_build(result.name, result.number) :: + text("last success: ") ::: link_build(result.name, result.id) :: text(" on " + result.date))) first_failed.toList ::: last_success.toList } def render_job(job: Job): XML.Body = - par(link_build(job.name, job.number) :: text(": running since " + job.start_date)) :: + par(link_build(job.name, job.id) :: text(": running since " + job.start_date)) :: render_if( finished.headOption.exists(_.status != Status.ok) && job.kind != User_Build.name, render_previous(finished)) def render_result(result: Result): XML.Body = par( - link_build(result.name, result.number) :: + link_build(result.name, result.id) :: text(" (" + result.status.toString + ") on " + result.date)) :: render_if(result.status != Status.ok && result.kind != User_Build.name, render_previous(finished.tail)) @@ -983,25 +983,25 @@ def render_overview(kind: String, state: State): XML.Body = render_page("Overview: " + kind + " job ") { def render_job(job: Job): XML.Body = - List(par(link_build(job.name, job.number) :: text(" running since " + job.start_date))) + List(par(link_build(job.name, job.id) :: text(" running since " + job.start_date))) def render_result(result: Result): XML.Body = List(par( - link_build(result.name, result.number) :: + link_build(result.name, result.id) :: text(" (" + result.status + ") on " + result.date))) itemize( - state.get_running(kind).sortBy(_.number).reverse.map(render_job) ::: - state.get_finished(kind).sortBy(_.number).reverse.map(render_result)) :: Nil + state.get_running(kind).sortBy(_.id).reverse.map(render_job) ::: + state.get_finished(kind).sortBy(_.id).reverse.map(render_result)) :: Nil } private val ID = Params.key(Markup.ID) def render_build(elem: T, state: State, public: Boolean): XML.Body = render_page("Build: " + elem.name) { - def render_cancel(id: UUID.T): XML.Body = + def render_cancel(uuid: UUID.T): XML.Body = render_if(!public, List( - submit_form("", List(hidden(ID, id.toString), + submit_form("", List(hidden(ID, uuid.toString), api_button(paths.api_route(API.BUILD_CANCEL), "cancel build"))))) def render_rev(isabelle_rev: String, components: List[Component]): XML.Body = @@ -1014,12 +1014,12 @@ case task: Task => par(text("Task from " + task.submit_date + ". ")) :: render_rev(task.isabelle_rev, task.components) ::: - render_cancel(task.id) + render_cancel(task.uuid) case job: Job => par(text("Start: " + job.start_date)) :: par( if (job.cancelled) text("Cancelling...") - else text("Running...") ::: render_cancel(job.id)) :: + else text("Running...") ::: render_cancel(job.uuid)) :: render_rev(job.isabelle_rev, job.components) ::: source(cache.lookup(store, job.name)) :: Nil case result: Result => @@ -1032,7 +1032,7 @@ def render_cancelled: XML.Body = List(chapter("Build Cancelled"), frontend_link(paths.frontend_url(Page.HOME), text("Home"))) - def parse_id(params: Params.Data): Option[UUID.T] = + def parse_uuid(params: Params.Data): Option[UUID.T] = for { id <- params.get(ID) uuid <- UUID.unapply(id) @@ -1055,18 +1055,18 @@ case Markup.Name(name) => val state = _state state.get(name).map(Model.Build(_, state)) - case Id(UUID(id)) => + case Id(UUID(uuid)) => val state = _state - state.get(id).map(Model.Build(_, state, public = false)) + state.get(uuid).map(Model.Build(_, state, public = false)) case _ => None } def cancel_build(params: Params.Data): Option[Model] = for { - id <- View.parse_id(params) + uuid <- View.parse_uuid(params) model <- synchronized_database("cancel_build") { - _state.get(id).map { + _state.get(uuid).map { case task: Task => _state = _state.remove_pending(task.name) Model.Cancelled @@ -1116,8 +1116,8 @@ /* context */ - case class Context(store: Store, task: Task, number: Long) { - def name = task.kind + "/" + number + case class Context(store: Store, task: Task, id: Long) { + def name = task.kind + "/" + id def progress: Progress = new File_Progress(store.log_file(name)) def task_dir: Path = store.task_dir(task) @@ -1210,7 +1210,7 @@ val pending = base_dir + Path.basic("pending") val finished = base_dir + Path.basic("finished") - def task_dir(task: Task) = pending + Path.basic(task.id.toString) + def task_dir(task: Task) = pending + Path.basic(task.uuid.toString) def log_file(name: String): Path = finished + Path.explode(name) def sync_permissions(dir: Path, ssh: SSH.System = SSH.Local): Unit = { @@ -1365,14 +1365,14 @@ rev: String = "", progress: Progress = new Progress ): UUID.T = { - val id = UUID.random() + val uuid = UUID.random() val afp_rev = if (afp_root.nonEmpty) Some("") else None val hosts_spec = options.string("build_manager_cluster") val build_config = User_Build(afp_rev, prefs, requirements, all_sessions, base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions, build_heap, clean_build, export_files, fresh_build, presentation, verbose) - val task = Task(build_config, hosts_spec, id, Date.now(), Priority.high) + val task = Task(build_config, hosts_spec, uuid, Date.now(), Priority.high) val dir = store.task_dir(task) @@ -1397,13 +1397,13 @@ } } } - val address = options.string("build_manager_address") + "/build?id=" + task.id + val address = options.string("build_manager_address") + "/build?id=" + task.uuid progress.echo("Submitted task. Private url: " + address) } } } - id + uuid }