diff -r 748f9bee8278 -r 433475f17d73 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Thu Jul 04 09:57:40 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Thu Jul 04 13:50:14 2024 +0200 @@ -21,7 +21,10 @@ case _ => error("Malformed component: " + quote(s)) } - def AFP(rev: String = "") = Component("AFP", rev) + val AFP = "AFP" + + def isabelle(rev: String = "") = Component("Isabelle", rev) + def afp(rev: String = "") = Component(AFP, rev) } case class Component(name: String, rev: String = "") { @@ -32,7 +35,7 @@ sealed trait Build_Config { def name: String - def components: List[Component] + def extra_components: List[Component] def fresh_build: Boolean def build_cluster: Boolean def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String @@ -47,7 +50,7 @@ isabelle_rev = "default") } - case class CI_Build(name: String, build_cluster: Boolean, components: List[Component]) + case class CI_Build(name: String, build_cluster: Boolean, extra_components: List[Component]) extends Build_Config { def fresh_build: Boolean = true def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = @@ -79,7 +82,7 @@ verbose: Boolean = false ) extends Build_Config { def name: String = User_Build.name - def components: List[Component] = afp_rev.map(Component.AFP).toList + def extra_components: List[Component] = afp_rev.map(Component.afp).toList def build_cluster: Boolean = true def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = { " build" + @@ -122,7 +125,8 @@ ) extends Build { def name: String = uuid.toString def kind: String = build_config.name - def components: List[Component] = build_config.components + def components: List[Component] = Component.isabelle(isabelle_rev) :: extra_components + def extra_components: List[Component] = build_config.extra_components def build_cluster = build_config.build_cluster def build_hosts: List[Build_Cluster.Host] = @@ -133,7 +137,6 @@ uuid: UUID.T, kind: String, id: Long, - isabelle_rev: String, build_cluster: Boolean, hostnames: List[String], components: List[Component], @@ -163,7 +166,11 @@ isabelle_version: Option[String], afp_version: Option[String], serial: Long = 0, - ) extends Build { def name: String = Build.name(kind, id) } + ) extends Build { + def name: String = Build.name(kind, id) + def components: List[Component] = + isabelle_version.map(Component.isabelle).toList ::: afp_version.map(Component.afp).toList + } object State { def max_serial(serials: Iterable[Long]): Long = serials.maxOption.getOrElse(0L) @@ -312,7 +319,7 @@ val submit_date = SQL.Column.date("submit_date") val priority = SQL.Column.string("priority") val isabelle_rev = SQL.Column.string("isabelle_rev") - val components = SQL.Column.string("components") + val extra_components = SQL.Column.string("extra_components") val prefs = SQL.Column.string("prefs") val requirements = SQL.Column.bool("requirements") @@ -331,9 +338,9 @@ val table = make_table(List(kind, build_cluster, hosts_spec, timeout, other_settings, 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), + priority, isabelle_rev, extra_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), name = "pending") } @@ -349,10 +356,11 @@ val submit_date = res.date(Pending.submit_date) val priority = Priority.valueOf(res.string(Pending.priority)) val isabelle_rev = res.string(Pending.isabelle_rev) - val components = space_explode(',', res.string(Pending.components)).map(Component.parse) + val extra_components = + space_explode(',', res.string(Pending.extra_components)).map(Component.parse) val build_config = - if (kind != User_Build.name) CI_Build(kind, build_cluster, components) + if (kind != User_Build.name) CI_Build(kind, build_cluster, extra_components) else { val prefs = Options.Spec.parse(res.string(Pending.prefs)) val requirements = res.bool(Pending.requirements) @@ -370,7 +378,7 @@ val presentation = res.bool(Pending.presentation) val verbose = res.bool(Pending.verbose) - val afp_rev = components.find(_.name == Component.AFP().name).map(_.rev) + val afp_rev = extra_components.find(_.name == Component.AFP).map(_.rev) 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) @@ -406,7 +414,7 @@ stmt.date(7) = task.submit_date stmt.string(8) = task.priority.toString stmt.string(9) = task.isabelle_rev - stmt.string(10) = task.components.mkString(",") + stmt.string(10) = task.extra_components.mkString(",") def get[A](f: User_Build => A): Option[A] = task.build_config match { @@ -441,7 +449,6 @@ val uuid = SQL.Column.string("uuid").make_primary_key val kind = SQL.Column.string("kind") 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") val components = SQL.Column.string("components") @@ -450,8 +457,8 @@ val cancelled = SQL.Column.bool("cancelled") val table = - make_table(List(uuid, kind, id, isabelle_rev, build_cluster, hostnames, components, timeout, - start_date, cancelled), + make_table(List(uuid, kind, id, build_cluster, hostnames, components, timeout, start_date, + cancelled), name = "running") } @@ -461,7 +468,6 @@ val uuid = res.string(Running.uuid) val kind = res.string(Running.kind) 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)) val components = space_explode(',', res.string(Running.components)).map(Component.parse) @@ -469,8 +475,8 @@ val start_date = res.date(Running.start_date) val cancelled = res.bool(Running.cancelled) - val job = Job(UUID.make(uuid), kind, id, isabelle_rev, build_cluster, hostnames, - components, timeout, start_date, cancelled) + val job = Job(UUID.make(uuid), kind, id, build_cluster, hostnames, components, timeout, + start_date, cancelled) job.name -> job }) @@ -493,13 +499,12 @@ stmt.string(1) = job.uuid.toString stmt.string(2) = job.kind stmt.long(3) = job.id - stmt.string(4) = job.isabelle_rev - stmt.bool(5) = job.build_cluster - stmt.string(6) = job.hostnames.mkString(",") - stmt.string(7) = job.components.mkString(",") - stmt.long(8) = job.timeout.ms - stmt.date(9) = job.start_date - stmt.bool(10) = job.cancelled + stmt.bool(4) = job.build_cluster + stmt.string(5) = job.hostnames.mkString(",") + stmt.string(6) = job.components.mkString(",") + stmt.long(7) = job.timeout.ms + stmt.date(8) = job.start_date + stmt.bool(9) = job.cancelled }) } update @@ -811,31 +816,29 @@ val hostnames = task.build_hosts.map(_.hostname).distinct - val components = - for (component <- task.components) - yield sync_dirs.find(_.name == component.name) match { + val extra_components = + for (extra_component <- task.extra_components) + yield sync_dirs.find(_.name == extra_component.name) match { case Some(sync_dir) => val target = context.task_dir + sync_dir.target - val rev = sync(sync_dir.hg, component.rev, target) + val rev = sync(sync_dir.hg, extra_component.rev, target) - if (!component.is_local) + if (!extra_component.is_local) File.append(context.task_dir + Sync.DIRS_ROOTS, sync_dir.roots_entry + "\n") - component.copy(rev = rev) + extra_component.copy(rev = rev) case None => - if (component.is_local) component - else error("Unknown component " + component) + if (extra_component.is_local) extra_component + else error("Unknown component " + extra_component) } - Job(task.uuid, task.kind, id, isabelle_rev, task.build_cluster, hostnames, components, - task.timeout, start_date) + Job(task.uuid, task.kind, id, task.build_cluster, hostnames, + Component.isabelle(isabelle_rev) :: extra_components, task.timeout, start_date) } match { case Exn.Res(job) => _state = _state.add_running(job) - for { - component <- Component("Isabelle", job.isabelle_rev) :: job.components - if !component.is_local - } context.report.progress.echo("Using " + component.toString) + for (component <- job.components if !component.is_local) + context.report.progress.echo("Using " + component.toString) Some(context) case Exn.Exn(exn) => @@ -1159,16 +1162,13 @@ 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 = - for { - component <- Component("Isabelle", isabelle_rev) :: components - if !component.is_local - } yield par(text(component.toString)) + def render_rev(components: List[Component]): XML.Body = + for (component <- components if !component.is_local) yield par(text(component.toString)) build match { case task: Task => par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) :: - render_rev(task.isabelle_rev, task.components) ::: + render_rev(task.components) ::: render_cancel(task.uuid) case job: Job => val report_data = cache.lookup(store.report(job.kind, job.id)) @@ -1177,7 +1177,7 @@ par( if (job.cancelled) text("Cancelling...") else text("Running...") ::: render_cancel(job.uuid)) :: - render_rev(job.isabelle_rev, job.components) ::: + render_rev(job.components) ::: source(report_data.log) :: Nil case result: Result => val report_data = cache.lookup(store.report(result.kind, result.id)) @@ -1319,8 +1319,8 @@ try { val init_components = for { - component <- task.build_config.components - target = _dir + Sync.DIRS + Path.basic(component.name) + extra_component <- task.build_config.extra_components + target = _dir + Sync.DIRS + Path.basic(extra_component.name) if Components.is_component_dir(target) } yield "init_component " + quote(target.absolute.implode)