718 |
718 |
719 |
719 |
720 /* repository poller */ |
720 /* repository poller */ |
721 |
721 |
722 object Poller { |
722 object Poller { |
723 case class State(ids: List[String], next: Future[List[String]]) |
723 case class Versions(isabelle: String, components: List[Component]) |
|
724 case class State(current: Versions, next: Future[Versions]) |
724 } |
725 } |
725 |
726 |
726 class Poller( |
727 class Poller( |
727 ci_jobs: List[String], |
728 ci_jobs: List[isabelle.CI_Build.Job], |
728 store: Store, |
729 store: Store, |
729 isabelle_repository: Mercurial.Repository, |
730 isabelle_repository: Mercurial.Repository, |
730 sync_dirs: List[Sync.Dir], |
731 sync_dirs: List[Sync.Dir], |
731 progress: Progress |
732 progress: Progress |
732 ) extends Loop_Process[Poller.State]("Poller", store, progress) { |
733 ) extends Loop_Process[Poller.State]("Poller", store, progress) { |
733 |
734 |
734 override def delay = options.seconds("build_manager_poll_delay") |
735 override def delay = options.seconds("build_manager_poll_delay") |
735 |
736 |
736 private def ids: List[String] = |
737 private def current: Poller.Versions = |
737 isabelle_repository.id("default") :: sync_dirs.map(_.hg.id("default")) |
738 Poller.Versions(isabelle_repository.id("default"), sync_dirs.map(dir => |
738 |
739 Component(dir.name, dir.hg.id("default")))) |
739 private def poll: Future[List[String]] = Future.fork { |
740 |
|
741 private def poll: Future[Poller.Versions] = Future.fork { |
740 Par_List.map((repo: Mercurial.Repository) => repo.pull(), |
742 Par_List.map((repo: Mercurial.Repository) => repo.pull(), |
741 isabelle_repository :: sync_dirs.map(_.hg)) |
743 isabelle_repository :: sync_dirs.map(_.hg)) |
742 |
744 |
743 ids |
745 current |
744 } |
746 } |
745 |
747 |
746 val init: Poller.State = Poller.State(ids, poll) |
748 val init: Poller.State = Poller.State(current, poll) |
747 |
749 |
748 def ci_task(name: String): Task = |
750 def ci_task(ci_job: isabelle.CI_Build.Job): Task = { |
749 Task(CI_Build(name, sync_dirs.map(dir => Component(dir.name, "default"))), |
751 val ci_build = CI_Build(ci_job.name, ci_job.components.map(Component(_, "default"))) |
750 priority = Priority.low, isabelle_rev = "default") |
752 Task(ci_build, priority = Priority.low, isabelle_rev = "default") |
751 |
753 } |
752 private def add_task(): Unit = synchronized_database("add_task") { |
754 |
753 for (name <- ci_jobs if !_state.pending.values.exists(_.kind == name)) { |
755 private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = { |
754 _state = _state.add_pending(ci_task(name)) |
756 val isabelle_updated = current.isabelle != next.isabelle |
|
757 val updated_components = |
|
758 next.components.zip(current.components).filter(_ != _).map(_._1.name).toSet |
|
759 |
|
760 synchronized_database("add_tasks") { |
|
761 for { |
|
762 ci_job <- ci_jobs |
|
763 if isabelle_updated || ci_job.components.exists(updated_components.contains) |
|
764 if !_state.pending.values.exists(_.kind == ci_job.name) |
|
765 } _state = _state.add_pending(ci_task(ci_job)) |
755 } |
766 } |
756 } |
767 } |
757 |
768 |
758 def loop_body(state: Poller.State): Poller.State = |
769 def loop_body(state: Poller.State): Poller.State = |
759 if (!state.next.is_finished) state |
770 if (!state.next.is_finished) state |
760 else { |
771 else { |
761 state.next.join_result match { |
772 state.next.join_result match { |
762 case Exn.Exn(exn) => |
773 case Exn.Exn(exn) => |
763 echo_error_message("Could not reach repository: " + exn.getMessage) |
774 echo_error_message("Could not reach repository: " + exn.getMessage) |
764 Poller.State(state.ids, poll) |
775 Poller.State(state.current, poll) |
765 case Exn.Res(ids1) => |
776 case Exn.Res(next) => |
766 if (state.ids != ids1) { |
777 if (state.current != next) { |
767 echo("Found new revisions: " + ids1) |
778 echo("Found new revisions: " + next) |
768 add_task() |
779 add_tasks(state.current, next) |
769 } |
780 } |
770 Poller.State(ids1, poll) |
781 Poller.State(next, poll) |
771 } |
782 } |
772 } |
783 } |
773 } |
784 } |
774 |
785 |
775 |
786 |
1151 sync_dirs: List[Sync.Dir] = Nil, |
1162 sync_dirs: List[Sync.Dir] = Nil, |
1152 progress: Progress = new Progress |
1163 progress: Progress = new Progress |
1153 ): Unit = { |
1164 ): Unit = { |
1154 val store = Store(options) |
1165 val store = Store(options) |
1155 val isabelle_repository = Mercurial.self_repository() |
1166 val isabelle_repository = Mercurial.self_repository() |
1156 val ci_jobs = space_explode(',', options.string("build_manager_ci_jobs")) |
1167 val ci_jobs = |
|
1168 space_explode(',', options.string("build_manager_ci_jobs")).map(isabelle.CI_Build.the_job) |
1157 val url = Url(options.string("build_manager_address")) |
1169 val url = Url(options.string("build_manager_address")) |
1158 val paths = Web_App.Paths(url, Path.current, true, Web_Server.Page.HOME) |
1170 val paths = Web_App.Paths(url, Path.current, true, Web_Server.Page.HOME) |
1159 |
1171 |
1160 using(store.open_database())(db => |
1172 using(store.open_database())(db => |
1161 Build_Manager.private_data.transaction_lock(db, |
1173 Build_Manager.private_data.transaction_lock(db, |