diff -r 06a473ad2777 -r ed9b1598d293 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Thu Jun 06 09:04:01 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Thu Jun 06 13:37:27 2024 +0200 @@ -720,11 +720,12 @@ /* repository poller */ object Poller { - case class State(ids: List[String], next: Future[List[String]]) + case class Versions(isabelle: String, components: List[Component]) + case class State(current: Versions, next: Future[Versions]) } class Poller( - ci_jobs: List[String], + ci_jobs: List[isabelle.CI_Build.Job], store: Store, isabelle_repository: Mercurial.Repository, sync_dirs: List[Sync.Dir], @@ -733,25 +734,35 @@ override def delay = options.seconds("build_manager_poll_delay") - private def ids: List[String] = - isabelle_repository.id("default") :: sync_dirs.map(_.hg.id("default")) + private def current: Poller.Versions = + Poller.Versions(isabelle_repository.id("default"), sync_dirs.map(dir => + Component(dir.name, dir.hg.id("default")))) - private def poll: Future[List[String]] = Future.fork { + private def poll: Future[Poller.Versions] = Future.fork { Par_List.map((repo: Mercurial.Repository) => repo.pull(), isabelle_repository :: sync_dirs.map(_.hg)) - ids + current + } + + val init: Poller.State = Poller.State(current, poll) + + def ci_task(ci_job: isabelle.CI_Build.Job): Task = { + val ci_build = CI_Build(ci_job.name, ci_job.components.map(Component(_, "default"))) + Task(ci_build, priority = Priority.low, isabelle_rev = "default") } - val init: Poller.State = Poller.State(ids, poll) + private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = { + val isabelle_updated = current.isabelle != next.isabelle + val updated_components = + next.components.zip(current.components).filter(_ != _).map(_._1.name).toSet - def ci_task(name: String): Task = - Task(CI_Build(name, sync_dirs.map(dir => Component(dir.name, "default"))), - priority = Priority.low, isabelle_rev = "default") - - private def add_task(): Unit = synchronized_database("add_task") { - for (name <- ci_jobs if !_state.pending.values.exists(_.kind == name)) { - _state = _state.add_pending(ci_task(name)) + synchronized_database("add_tasks") { + for { + ci_job <- ci_jobs + if isabelle_updated || ci_job.components.exists(updated_components.contains) + if !_state.pending.values.exists(_.kind == ci_job.name) + } _state = _state.add_pending(ci_task(ci_job)) } } @@ -761,13 +772,13 @@ state.next.join_result match { case Exn.Exn(exn) => echo_error_message("Could not reach repository: " + exn.getMessage) - Poller.State(state.ids, poll) - case Exn.Res(ids1) => - if (state.ids != ids1) { - echo("Found new revisions: " + ids1) - add_task() + Poller.State(state.current, poll) + case Exn.Res(next) => + if (state.current != next) { + echo("Found new revisions: " + next) + add_tasks(state.current, next) } - Poller.State(ids1, poll) + Poller.State(next, poll) } } } @@ -1153,7 +1164,8 @@ ): Unit = { val store = Store(options) val isabelle_repository = Mercurial.self_repository() - val ci_jobs = space_explode(',', options.string("build_manager_ci_jobs")) + val ci_jobs = + space_explode(',', options.string("build_manager_ci_jobs")).map(isabelle.CI_Build.the_job) val url = Url(options.string("build_manager_address")) val paths = Web_App.Paths(url, Path.current, true, Web_Server.Page.HOME)