# HG changeset patch # User Fabian Huch # Date 1717678288 -7200 # Node ID e3f472221f8f4053a728bfba96bdeea57fe20ca8 # Parent ed9b1598d293e52bf6d06e39aad9ced72619d97f add triggers to ci jobs: on commit vs timed; diff -r ed9b1598d293 -r e3f472221f8f src/Pure/Admin/ci_build.scala --- a/src/Pure/Admin/ci_build.scala Thu Jun 06 13:37:27 2024 +0200 +++ b/src/Pure/Admin/ci_build.scala Thu Jun 06 14:51:28 2024 +0200 @@ -64,12 +64,28 @@ /* ci build jobs */ + sealed trait Trigger + case object On_Commit extends Trigger + + object Timed { + def nightly(start_time: Time = Time.zero): Timed = + Timed { (before, now) => + val start0 = before.midnight + start_time + val start1 = now.midnight + start_time + (before.time < start0.time && start0.time <= now.time) || + (before.time < start1.time && start1.time <= now.time) + } + } + + case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger + sealed case class Job( name: String, description: String, profile: Profile, config: Build_Config, - components: List[String] = Nil + components: List[String] = Nil, + trigger: Trigger = On_Commit ) { override def toString: String = name } diff -r ed9b1598d293 -r e3f472221f8f src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Thu Jun 06 13:37:27 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Thu Jun 06 14:51:28 2024 +0200 @@ -35,6 +35,11 @@ def command(build_hosts: List[Build_Cluster.Host]): String } + object CI_Build { + def apply(job: isabelle.CI_Build.Job): CI_Build = + CI_Build(job.name, job.components.map(Component(_, "default"))) + } + case class CI_Build(name: String, components: List[Component]) extends Build_Config { def fresh_build: Boolean = true def command(build_hosts: List[Build_Cluster.Host]): String = " ci_build " + name @@ -747,11 +752,6 @@ 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") - } - private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = { val isabelle_updated = current.isabelle != next.isabelle val updated_components = @@ -760,9 +760,13 @@ synchronized_database("add_tasks") { for { ci_job <- ci_jobs + if ci_job.trigger == isabelle.CI_Build.On_Commit 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)) + } { + val task = Task(CI_Build(ci_job), priority = Priority.low, isabelle_rev = "default") + _state = _state.add_pending(task) + } } } @@ -783,6 +787,31 @@ } } + class Timer( + ci_jobs: List[isabelle.CI_Build.Job], + store: Store, + isabelle_repository: Mercurial.Repository, + sync_dirs: List[Sync.Dir], + progress: Progress + ) extends Loop_Process[Date]("Timer", store, progress) { + + private def add_tasks(previous: Date, next: Date): Unit = + for (ci_job <-ci_jobs) + ci_job.trigger match { + case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) => + val task = Task(CI_Build(ci_job), isabelle_rev = "default") + _state = _state.add_pending(task) + case _ => + } + + def init: Date = Date.now() + def loop_body(previous: Date): Date = { + val now = Date.now() + add_tasks(previous, now) + now + } + } + /* web server */ @@ -1176,6 +1205,7 @@ val processes = List( new Runner(store, build_hosts, isabelle_repository, sync_dirs, progress), new Poller(ci_jobs, store, isabelle_repository, sync_dirs, progress), + new Timer(ci_jobs, store, isabelle_repository, sync_dirs, progress), new Web_Server(port, paths, store, progress)) val threads = processes.map(Isabelle_Thread.create(_))