# HG changeset patch # User Fabian Huch # Date 1718205133 -7200 # Node ID a7f8249533e90201267a090b7da4ed71d86986c6 # Parent a9fce67fb8b29851ddfa62cb1f9cb079188a0658 moved ci_build module to build_ci; diff -r a9fce67fb8b2 -r a7f8249533e9 etc/build.props --- a/etc/build.props Wed Jun 12 17:06:34 2024 +0200 +++ b/etc/build.props Wed Jun 12 17:12:13 2024 +0200 @@ -17,7 +17,6 @@ src/Pure/Admin/build_release.scala \ src/Pure/Admin/build_status.scala \ src/Pure/Admin/check_sources.scala \ - src/Pure/Admin/ci_build.scala \ src/Pure/Admin/component_bash_process.scala \ src/Pure/Admin/component_csdp.scala \ src/Pure/Admin/component_cvc5.scala \ @@ -54,6 +53,7 @@ src/Pure/Build/browser_info.scala \ src/Pure/Build/build.scala \ src/Pure/Build/build_benchmark.scala \ + src/Pure/Build/build_ci.scala \ src/Pure/Build/build_cluster.scala \ src/Pure/Build/build_job.scala \ src/Pure/Build/build_process.scala \ diff -r a9fce67fb8b2 -r a7f8249533e9 src/Pure/Admin/ci_build.scala --- a/src/Pure/Admin/ci_build.scala Wed Jun 12 17:06:34 2024 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,267 +0,0 @@ -/* Title: Pure/Admin/ci_build.scala - Author: Fabian Huch, TU Munich - -Module for automated (continuous integration) builds. -*/ - -package isabelle - - -import scala.collection.mutable - - -object CI_Build { - def section(title: String): String = "\n=== " + title + " ===\n" - - - /* mailing */ - - object Mail_System { - def try_open(options: Options): Option[Mail_System] = - Exn.capture(new Mail_System(options)) match { - case Exn.Res(res) if res.server.defined => Some(res) - case _ => None - } - } - - class Mail_System private(options: Options) { - val from: Mail.Address = Mail.address(options.string("ci_mail_from")) - val to: Mail.Address = Mail.address(options.string("ci_mail_to")) - - val server: Mail.Server = - new Mail.Server(Mail.address(options.string("ci_mail_sender")), - smtp_host = options.string("ci_mail_smtp_host"), - smtp_port = options.int("ci_mail_smtp_port"), - user = options.string("ci_mail_user"), - password = options.string("ci_mail_password")) - } - - - /** ci build jobs **/ - - /* hosts */ - - sealed trait Hosts { - def hosts_spec: String - def max_jobs: Option[Int] - def prefs: List[Options.Spec] - def numa_shuffling: Boolean - def build_cluster: Boolean - } - - case class Local(host_spec: String, jobs: Int, threads: Int, numa_shuffling: Boolean = true) - extends Hosts { - def hosts_spec: String = host_spec - def max_jobs: Option[Int] = Some(jobs) - def prefs: List[Options.Spec] = List(Options.Spec.eq("threads", threads.toString)) - def build_cluster: Boolean = false - } - - case class Cluster(hosts_spec: String, numa_shuffling: Boolean = true) extends Hosts { - def max_jobs: Option[Int] = None - def prefs: List[Options.Spec] = Nil - def build_cluster: Boolean = true - } - - - /* build triggers */ - - 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 - - - /* build hooks */ - - trait Hook { - def pre(options: Options, progress: Progress): Unit = () - def post( - options: Options, - start_date: Date, - url: Option[Url], - results: Build.Results, - progress: Progress - ): Unit = () - } - - object none extends Hook - - - /* jobs */ - - sealed case class Job( - name: String, - description: String, - hosts: Hosts, - afp: Boolean = false, - selection: Sessions.Selection = Sessions.Selection.empty, - presentation: Boolean = false, - clean_build: Boolean = false, - select_dirs: List[Path] = Nil, - build_prefs: List[Options.Spec] = Nil, - hook: Hook = none, - extra_components: List[String] = Nil, - trigger: Trigger = On_Commit - ) { - override def toString: String = name - - def afp_root: Option[Path] = if (!afp) None else Some(AFP.BASE) - - def prefs: List[Options.Spec] = build_prefs ++ hosts.prefs ++ document_prefs - def document_prefs: List[Options.Spec] = - if (!presentation) Nil - else List( - Options.Spec.eq("browser_info", "true"), - Options.Spec.eq("document", "pdf"), - Options.Spec.eq("document_variants", "document:outline=/proof,/ML")) - - def components: List[String] = (if (!afp) Nil else List("AFP")) ::: extra_components - } - - private lazy val known_jobs: List[Job] = - Isabelle_System.make_services(classOf[Isabelle_CI_Jobs]).flatMap(_.jobs) - - def show_jobs: String = - cat_lines(known_jobs.sortBy(_.name).map(job => job.name + " - " + job.description)) - - def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse - error("Unknown job " + quote(name)) - - - /* concrete jobs */ - - val timing = - Job("benchmark", - description = "runs benchmark and timing sessions", - Local("benchmark", jobs = 1, threads = 6, numa_shuffling = false), - selection = Sessions.Selection(session_groups = List("timing")), - clean_build = true, - select_dirs = List(Path.explode("~~/src/Benchmarks")), - trigger = Timed.nightly()) - - - /* ci build */ - - def ci_build( - options: Options, - job: Job, - build_hosts: List[Build_Cluster.Host] = Nil, - url: Option[Url] = None, - progress: Progress = new Progress - ): Unit = { - val start_date = Date.now() - - def return_code(f: => Unit): Int = - Exn.capture(f) match { - case Exn.Res(_) => Process_Result.RC.ok - case Exn.Exn(e) => - progress.echo_error_message(e.getMessage) - Process_Result.RC.error - } - - val mail_result = - return_code { - Mail_System.try_open(options).getOrElse(error("No mail configuration")).server.check() - } - - val pre_result = return_code { job.hook.pre(options, progress) } - - progress.echo(section("BUILD")) - val results = progress.interrupt_handler { - Build.build( - options ++ job.prefs, - build_hosts = build_hosts, - selection = job.selection, - progress = progress, - clean_build = job.clean_build, - afp_root = job.afp_root, - select_dirs = job.select_dirs, - numa_shuffling = job.hosts.numa_shuffling, - max_jobs = job.hosts.max_jobs) - } - - val post_result = return_code { job.hook.post(options, start_date, url, results, progress) } - - val rc = List(mail_result, pre_result, results.rc, post_result).max - if (rc != Process_Result.RC.ok) { - progress.echo(section("FAILED")) - - if (mail_result != Process_Result.RC.ok) progress.echo("Mail: FAILED") - else { - val mail_system = Mail_System.try_open(options).get - val content = - "The job " + job.name + " failed. " + if_proper(url, " View the build at: " + url.get) - val mail = Mail("Build failed", List(mail_system.to), content, Some(mail_system.from)) - mail_system.server.send(mail) - } - - if (pre_result != Process_Result.RC.ok) progress.echo("Pre-hook: FAILED") - for (name <- results.sessions) { - if (results.cancelled(name)) progress.echo("Session " + name + ": CANCELLED") - else { - val result = results(name) - if (!result.ok) progress.echo("Session " + name + ": FAILED " + result.rc) - } - } - if (post_result != Process_Result.RC.ok) progress.echo("Post-hook: FAILED") - } - - sys.exit(rc) - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = Isabelle_Tool("ci_build", "builds Isabelle jobs in ci environments", - Scala_Project.here, - { args => - var options = Options.init() - val build_hosts = new mutable.ListBuffer[Build_Cluster.Host] - var url: Option[Url] = None - - val getopts = Getopts(""" -Usage: isabelle ci_build [OPTIONS] JOB - - Options are: - -H HOSTS host specifications of the form NAMES:PARAMETERS (separated by commas) - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -u URL build url - - Runs Isabelle builds in ci environment. For cluster builds, build hosts must - be passed explicitly (no registry). - - The following build jobs are available: - -""" + Library.indent_lines(4, show_jobs) + "\n", - "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.load(Nil), arg)), - "o:" -> (arg => options = options + arg), - "u:" -> (arg => url = Some(Url(arg)))) - - val more_args = getopts(args) - - val job = - more_args match { - case job :: Nil => the_job(job) - case _ => getopts.usage() - } - - val progress = new Console_Progress(verbose = true) - - ci_build(options, job, url = url, build_hosts = build_hosts.toList, progress = progress) - }) -} - -class Isabelle_CI_Jobs(val jobs: CI_Build.Job*) extends Isabelle_System.Service - -class CI_Jobs extends Isabelle_CI_Jobs(CI_Build.timing) diff -r a9fce67fb8b2 -r a7f8249533e9 src/Pure/Build/build_ci.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Build/build_ci.scala Wed Jun 12 17:12:13 2024 +0200 @@ -0,0 +1,267 @@ +/* Title: Pure/Build/build_ci.scala + Author: Fabian Huch, TU Munich + +Module for automated (continuous integration) builds. +*/ + +package isabelle + + +import scala.collection.mutable + + +object Build_CI { + def section(title: String): String = "\n=== " + title + " ===\n" + + + /* mailing */ + + object Mail_System { + def try_open(options: Options): Option[Mail_System] = + Exn.capture(new Mail_System(options)) match { + case Exn.Res(res) if res.server.defined => Some(res) + case _ => None + } + } + + class Mail_System private(options: Options) { + val from: Mail.Address = Mail.address(options.string("ci_mail_from")) + val to: Mail.Address = Mail.address(options.string("ci_mail_to")) + + val server: Mail.Server = + new Mail.Server(Mail.address(options.string("ci_mail_sender")), + smtp_host = options.string("ci_mail_smtp_host"), + smtp_port = options.int("ci_mail_smtp_port"), + user = options.string("ci_mail_user"), + password = options.string("ci_mail_password")) + } + + + /** ci build jobs **/ + + /* hosts */ + + sealed trait Hosts { + def hosts_spec: String + def max_jobs: Option[Int] + def prefs: List[Options.Spec] + def numa_shuffling: Boolean + def build_cluster: Boolean + } + + case class Local(host_spec: String, jobs: Int, threads: Int, numa_shuffling: Boolean = true) + extends Hosts { + def hosts_spec: String = host_spec + def max_jobs: Option[Int] = Some(jobs) + def prefs: List[Options.Spec] = List(Options.Spec.eq("threads", threads.toString)) + def build_cluster: Boolean = false + } + + case class Cluster(hosts_spec: String, numa_shuffling: Boolean = true) extends Hosts { + def max_jobs: Option[Int] = None + def prefs: List[Options.Spec] = Nil + def build_cluster: Boolean = true + } + + + /* build triggers */ + + 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 + + + /* build hooks */ + + trait Hook { + def pre(options: Options, progress: Progress): Unit = () + def post( + options: Options, + start_date: Date, + url: Option[Url], + results: Build.Results, + progress: Progress + ): Unit = () + } + + object none extends Hook + + + /* jobs */ + + sealed case class Job( + name: String, + description: String, + hosts: Hosts, + afp: Boolean = false, + selection: Sessions.Selection = Sessions.Selection.empty, + presentation: Boolean = false, + clean_build: Boolean = false, + select_dirs: List[Path] = Nil, + build_prefs: List[Options.Spec] = Nil, + hook: Hook = none, + extra_components: List[String] = Nil, + trigger: Trigger = On_Commit + ) { + override def toString: String = name + + def afp_root: Option[Path] = if (!afp) None else Some(AFP.BASE) + + def prefs: List[Options.Spec] = build_prefs ++ hosts.prefs ++ document_prefs + def document_prefs: List[Options.Spec] = + if (!presentation) Nil + else List( + Options.Spec.eq("browser_info", "true"), + Options.Spec.eq("document", "pdf"), + Options.Spec.eq("document_variants", "document:outline=/proof,/ML")) + + def components: List[String] = (if (!afp) Nil else List("AFP")) ::: extra_components + } + + private lazy val known_jobs: List[Job] = + Isabelle_System.make_services(classOf[Isabelle_CI_Jobs]).flatMap(_.jobs) + + def show_jobs: String = + cat_lines(known_jobs.sortBy(_.name).map(job => job.name + " - " + job.description)) + + def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse + error("Unknown job " + quote(name)) + + + /* concrete jobs */ + + val timing = + Job("benchmark", + description = "runs benchmark and timing sessions", + Local("benchmark", jobs = 1, threads = 6, numa_shuffling = false), + selection = Sessions.Selection(session_groups = List("timing")), + clean_build = true, + select_dirs = List(Path.explode("~~/src/Benchmarks")), + trigger = Timed.nightly()) + + + /* build ci */ + + def build_ci( + options: Options, + job: Job, + build_hosts: List[Build_Cluster.Host] = Nil, + url: Option[Url] = None, + progress: Progress = new Progress + ): Unit = { + val start_date = Date.now() + + def return_code(f: => Unit): Int = + Exn.capture(f) match { + case Exn.Res(_) => Process_Result.RC.ok + case Exn.Exn(e) => + progress.echo_error_message(e.getMessage) + Process_Result.RC.error + } + + val mail_result = + return_code { + Mail_System.try_open(options).getOrElse(error("No mail configuration")).server.check() + } + + val pre_result = return_code { job.hook.pre(options, progress) } + + progress.echo(section("BUILD")) + val results = progress.interrupt_handler { + Build.build( + options ++ job.prefs, + build_hosts = build_hosts, + selection = job.selection, + progress = progress, + clean_build = job.clean_build, + afp_root = job.afp_root, + select_dirs = job.select_dirs, + numa_shuffling = job.hosts.numa_shuffling, + max_jobs = job.hosts.max_jobs) + } + + val post_result = return_code { job.hook.post(options, start_date, url, results, progress) } + + val rc = List(mail_result, pre_result, results.rc, post_result).max + if (rc != Process_Result.RC.ok) { + progress.echo(section("FAILED")) + + if (mail_result != Process_Result.RC.ok) progress.echo("Mail: FAILED") + else { + val mail_system = Mail_System.try_open(options).get + val content = + "The job " + job.name + " failed. " + if_proper(url, " View the build at: " + url.get) + val mail = Mail("Build failed", List(mail_system.to), content, Some(mail_system.from)) + mail_system.server.send(mail) + } + + if (pre_result != Process_Result.RC.ok) progress.echo("Pre-hook: FAILED") + for (name <- results.sessions) { + if (results.cancelled(name)) progress.echo("Session " + name + ": CANCELLED") + else { + val result = results(name) + if (!result.ok) progress.echo("Session " + name + ": FAILED " + result.rc) + } + } + if (post_result != Process_Result.RC.ok) progress.echo("Post-hook: FAILED") + } + + sys.exit(rc) + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = Isabelle_Tool("build_ci", "builds Isabelle jobs in ci environments", + Scala_Project.here, + { args => + var options = Options.init() + val build_hosts = new mutable.ListBuffer[Build_Cluster.Host] + var url: Option[Url] = None + + val getopts = Getopts(""" +Usage: isabelle build_ci [OPTIONS] JOB + + Options are: + -H HOSTS host specifications of the form NAMES:PARAMETERS (separated by commas) + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -u URL build url + + Runs Isabelle builds in ci environment. For cluster builds, build hosts must + be passed explicitly (no registry). + + The following build jobs are available: + +""" + Library.indent_lines(4, show_jobs) + "\n", + "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.load(Nil), arg)), + "o:" -> (arg => options = options + arg), + "u:" -> (arg => url = Some(Url(arg)))) + + val more_args = getopts(args) + + val job = + more_args match { + case job :: Nil => the_job(job) + case _ => getopts.usage() + } + + val progress = new Console_Progress(verbose = true) + + build_ci(options, job, url = url, build_hosts = build_hosts.toList, progress = progress) + }) +} + +class Isabelle_CI_Jobs(val jobs: Build_CI.Job*) extends Isabelle_System.Service + +class CI_Jobs extends Isabelle_CI_Jobs(Build_CI.timing) diff -r a9fce67fb8b2 -r a7f8249533e9 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Wed Jun 12 17:06:34 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Wed Jun 12 17:12:13 2024 +0200 @@ -39,7 +39,7 @@ } object CI_Build { - def apply(job: isabelle.CI_Build.Job): CI_Build = + def apply(job: Build_CI.Job): CI_Build = CI_Build(job.name, job.hosts.build_cluster, job.components.map(Component(_, "default"))) } @@ -47,7 +47,7 @@ extends Build_Config { def fresh_build: Boolean = true def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = - " ci_build" + + " build_ci" + " -u " + Bash.string(job_url.toString) + if_proper(build_cluster, build_hosts.map(host => " -H " + Bash.string(host.print)).mkString) + " " + name @@ -851,7 +851,7 @@ } class Poller( - ci_jobs: List[isabelle.CI_Build.Job], + ci_jobs: List[Build_CI.Job], store: Store, isabelle_repository: Mercurial.Repository, sync_dirs: List[Sync.Dir], @@ -881,7 +881,7 @@ synchronized_database("add_tasks") { for { ci_job <- ci_jobs - if ci_job.trigger == isabelle.CI_Build.On_Commit + if ci_job.trigger == Build_CI.On_Commit if isabelle_updated || ci_job.components.exists(updated_components.contains) if !_state.pending.values.exists(_.kind == ci_job.name) } { @@ -910,7 +910,7 @@ } class Timer( - ci_jobs: List[isabelle.CI_Build.Job], + ci_jobs: List[Build_CI.Job], store: Store, isabelle_repository: Mercurial.Repository, sync_dirs: List[Sync.Dir], @@ -922,7 +922,7 @@ private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") { for (ci_job <- ci_jobs) ci_job.trigger match { - case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) => + case Build_CI.Timed(in_interval) if in_interval(previous, next) => val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, isabelle_rev = "default") echo("Triggered task " + task.kind) _state = _state.add_pending(task) @@ -1354,8 +1354,7 @@ ): Unit = { val store = Store(options) val isabelle_repository = Mercurial.self_repository() - val ci_jobs = - space_explode(',', options.string("build_manager_ci_jobs")).map(isabelle.CI_Build.the_job) + val ci_jobs = space_explode(',', options.string("build_manager_ci_jobs")).map(Build_CI.the_job) progress.echo_if(ci_jobs.nonEmpty, "Managing ci jobs: " + commas_quote(ci_jobs.map(_.name))) diff -r a9fce67fb8b2 -r a7f8249533e9 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Wed Jun 12 17:06:34 2024 +0200 +++ b/src/Pure/System/isabelle_tool.scala Wed Jun 12 17:12:13 2024 +0200 @@ -131,7 +131,7 @@ Build_Manager.isabelle_tool1, Build_Manager.isabelle_tool2, Build_Schedule.isabelle_tool, - CI_Build.isabelle_tool, + Build_CI.isabelle_tool, Doc.isabelle_tool, Docker_Build.isabelle_tool, Document_Build.isabelle_tool,