31 sealed trait Build_Config { |
31 sealed trait Build_Config { |
32 def name: String |
32 def name: String |
33 def components: List[Component] |
33 def components: List[Component] |
34 def fresh_build: Boolean |
34 def fresh_build: Boolean |
35 def command(build_hosts: List[Build_Cluster.Host]): String |
35 def command(build_hosts: List[Build_Cluster.Host]): String |
|
36 } |
|
37 |
|
38 object CI_Build { |
|
39 def apply(job: isabelle.CI_Build.Job): CI_Build = |
|
40 CI_Build(job.name, job.components.map(Component(_, "default"))) |
36 } |
41 } |
37 |
42 |
38 case class CI_Build(name: String, components: List[Component]) extends Build_Config { |
43 case class CI_Build(name: String, components: List[Component]) extends Build_Config { |
39 def fresh_build: Boolean = true |
44 def fresh_build: Boolean = true |
40 def command(build_hosts: List[Build_Cluster.Host]): String = " ci_build " + name |
45 def command(build_hosts: List[Build_Cluster.Host]): String = " ci_build " + name |
745 current |
750 current |
746 } |
751 } |
747 |
752 |
748 val init: Poller.State = Poller.State(current, poll) |
753 val init: Poller.State = Poller.State(current, poll) |
749 |
754 |
750 def ci_task(ci_job: isabelle.CI_Build.Job): Task = { |
|
751 val ci_build = CI_Build(ci_job.name, ci_job.components.map(Component(_, "default"))) |
|
752 Task(ci_build, priority = Priority.low, isabelle_rev = "default") |
|
753 } |
|
754 |
|
755 private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = { |
755 private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = { |
756 val isabelle_updated = current.isabelle != next.isabelle |
756 val isabelle_updated = current.isabelle != next.isabelle |
757 val updated_components = |
757 val updated_components = |
758 next.components.zip(current.components).filter(_ != _).map(_._1.name).toSet |
758 next.components.zip(current.components).filter(_ != _).map(_._1.name).toSet |
759 |
759 |
760 synchronized_database("add_tasks") { |
760 synchronized_database("add_tasks") { |
761 for { |
761 for { |
762 ci_job <- ci_jobs |
762 ci_job <- ci_jobs |
|
763 if ci_job.trigger == isabelle.CI_Build.On_Commit |
763 if isabelle_updated || ci_job.components.exists(updated_components.contains) |
764 if isabelle_updated || ci_job.components.exists(updated_components.contains) |
764 if !_state.pending.values.exists(_.kind == ci_job.name) |
765 if !_state.pending.values.exists(_.kind == ci_job.name) |
765 } _state = _state.add_pending(ci_task(ci_job)) |
766 } { |
|
767 val task = Task(CI_Build(ci_job), priority = Priority.low, isabelle_rev = "default") |
|
768 _state = _state.add_pending(task) |
|
769 } |
766 } |
770 } |
767 } |
771 } |
768 |
772 |
769 def loop_body(state: Poller.State): Poller.State = |
773 def loop_body(state: Poller.State): Poller.State = |
770 if (!state.next.is_finished) state |
774 if (!state.next.is_finished) state |
779 add_tasks(state.current, next) |
783 add_tasks(state.current, next) |
780 } |
784 } |
781 Poller.State(next, poll) |
785 Poller.State(next, poll) |
782 } |
786 } |
783 } |
787 } |
|
788 } |
|
789 |
|
790 class Timer( |
|
791 ci_jobs: List[isabelle.CI_Build.Job], |
|
792 store: Store, |
|
793 isabelle_repository: Mercurial.Repository, |
|
794 sync_dirs: List[Sync.Dir], |
|
795 progress: Progress |
|
796 ) extends Loop_Process[Date]("Timer", store, progress) { |
|
797 |
|
798 private def add_tasks(previous: Date, next: Date): Unit = |
|
799 for (ci_job <-ci_jobs) |
|
800 ci_job.trigger match { |
|
801 case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) => |
|
802 val task = Task(CI_Build(ci_job), isabelle_rev = "default") |
|
803 _state = _state.add_pending(task) |
|
804 case _ => |
|
805 } |
|
806 |
|
807 def init: Date = Date.now() |
|
808 def loop_body(previous: Date): Date = { |
|
809 val now = Date.now() |
|
810 add_tasks(previous, now) |
|
811 now |
|
812 } |
784 } |
813 } |
785 |
814 |
786 |
815 |
787 /* web server */ |
816 /* web server */ |
788 |
817 |
1174 create = true, label = "Build_Manager.build_manager") { store.init_dirs() }) |
1203 create = true, label = "Build_Manager.build_manager") { store.init_dirs() }) |
1175 |
1204 |
1176 val processes = List( |
1205 val processes = List( |
1177 new Runner(store, build_hosts, isabelle_repository, sync_dirs, progress), |
1206 new Runner(store, build_hosts, isabelle_repository, sync_dirs, progress), |
1178 new Poller(ci_jobs, store, isabelle_repository, sync_dirs, progress), |
1207 new Poller(ci_jobs, store, isabelle_repository, sync_dirs, progress), |
|
1208 new Timer(ci_jobs, store, isabelle_repository, sync_dirs, progress), |
1179 new Web_Server(port, paths, store, progress)) |
1209 new Web_Server(port, paths, store, progress)) |
1180 |
1210 |
1181 val threads = processes.map(Isabelle_Thread.create(_)) |
1211 val threads = processes.map(Isabelle_Thread.create(_)) |
1182 POSIX_Interrupt.handler { |
1212 POSIX_Interrupt.handler { |
1183 progress.stop() |
1213 progress.stop() |