diff -r a9fce67fb8b2 -r a7f8249533e9 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Wed Jun 12 17:06:34 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Wed Jun 12 17:12:13 2024 +0200 @@ -39,7 +39,7 @@ } object CI_Build { - def apply(job: isabelle.CI_Build.Job): CI_Build = + def apply(job: Build_CI.Job): CI_Build = CI_Build(job.name, job.hosts.build_cluster, job.components.map(Component(_, "default"))) } @@ -47,7 +47,7 @@ extends Build_Config { def fresh_build: Boolean = true def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = - " ci_build" + + " build_ci" + " -u " + Bash.string(job_url.toString) + if_proper(build_cluster, build_hosts.map(host => " -H " + Bash.string(host.print)).mkString) + " " + name @@ -851,7 +851,7 @@ } class Poller( - ci_jobs: List[isabelle.CI_Build.Job], + ci_jobs: List[Build_CI.Job], store: Store, isabelle_repository: Mercurial.Repository, sync_dirs: List[Sync.Dir], @@ -881,7 +881,7 @@ synchronized_database("add_tasks") { for { ci_job <- ci_jobs - if ci_job.trigger == isabelle.CI_Build.On_Commit + if ci_job.trigger == Build_CI.On_Commit if isabelle_updated || ci_job.components.exists(updated_components.contains) if !_state.pending.values.exists(_.kind == ci_job.name) } { @@ -910,7 +910,7 @@ } class Timer( - ci_jobs: List[isabelle.CI_Build.Job], + ci_jobs: List[Build_CI.Job], store: Store, isabelle_repository: Mercurial.Repository, sync_dirs: List[Sync.Dir], @@ -922,7 +922,7 @@ private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") { for (ci_job <- ci_jobs) ci_job.trigger match { - case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) => + case Build_CI.Timed(in_interval) if in_interval(previous, next) => val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, isabelle_rev = "default") echo("Triggered task " + task.kind) _state = _state.add_pending(task) @@ -1354,8 +1354,7 @@ ): Unit = { val store = Store(options) val isabelle_repository = Mercurial.self_repository() - val ci_jobs = - space_explode(',', options.string("build_manager_ci_jobs")).map(isabelle.CI_Build.the_job) + val ci_jobs = space_explode(',', options.string("build_manager_ci_jobs")).map(Build_CI.the_job) progress.echo_if(ci_jobs.nonEmpty, "Managing ci jobs: " + commas_quote(ci_jobs.map(_.name)))