--- 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
}
--- 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(_))