--- 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 \
--- 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)
--- /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)
--- 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)))
--- 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,