--- a/src/Pure/Admin/ci_build.scala Tue Jun 25 18:09:53 2024 +0200
+++ b/src/Pure/Admin/ci_build.scala Wed Jun 12 17:06:34 2024 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/Admin/ci_build.scala
- Author: Lars Hupel and Fabian Huch, TU Munich
+ Author: Fabian Huch, TU Munich
-Build profile for continuous integration services.
+Module for automated (continuous integration) builds.
*/
package isabelle
@@ -9,48 +9,37 @@
import scala.collection.mutable
-import java.time.ZoneId
-import java.time.format.DateTimeFormatter
-import java.util.{Properties => JProperties, Map => JMap}
-import java.nio.file.Files
-
object CI_Build {
- /* build result */
+ def section(title: String): String = "\n=== " + title + " ===\n"
+
+
+ /* mailing */
- case class Result(rc: Int)
- case object Result {
- def ok: Result = Result(Process_Result.RC.ok)
- def error: Result = Result(Process_Result.RC.error)
+ 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"))
}
- /* build config */
-
- case class Build_Config(
- documents: Boolean = true,
- clean: Boolean = true,
- include: List[Path] = Nil,
- select: List[Path] = Nil,
- pre_hook: Options => Result = _ => Result.ok,
- post_hook: (Build.Results, Options, Time) => Result = (_, _, _) => Result.ok,
- selection: Sessions.Selection = Sessions.Selection.empty)
-
+ /** ci build jobs **/
- def mail_server(options: Options): Mail.Server = {
- val sender =
- proper_string(options.string("ci_mail_sender")).map(Mail.address) getOrElse
- Mail.default_address
-
- new Mail.Server(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
@@ -74,6 +63,9 @@
def build_cluster: Boolean = true
}
+
+ /* build triggers */
+
sealed trait Trigger
case object On_Commit extends Trigger
@@ -89,19 +81,56 @@
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,
- config: Build_Config,
- components: List[String] = Nil,
+ 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_Builds]).flatMap(_.jobs)
+ 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))
@@ -109,135 +138,86 @@
def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse
error("Unknown job " + quote(name))
- val timing =
- Job(
- "benchmark", "runs benchmark and timing sessions",
- Local("benchmark", jobs = 1, threads = 6, numa_shuffling = false),
- Build_Config(
- documents = false,
- select = List(
- Path.explode("$ISABELLE_HOME/src/Benchmarks")),
- selection = Sessions.Selection(session_groups = List("timing"))))
-
- /* session status */
+ /* concrete jobs */
- sealed abstract class Status(val str: String) {
- def merge(that: Status): Status = (this, that) match {
- case (Ok, s) => s
- case (Failed, _) => Failed
- case (Skipped, Failed) => Failed
- case (Skipped, _) => Skipped
- }
- }
-
- object Status {
- def merge(statuses: List[Status]): Status =
- statuses.foldLeft(Ok: Status)(_ merge _)
-
- def from_results(results: Build.Results, session: String): Status =
- if (results.cancelled(session)) Skipped
- else if (results(session).ok) Ok
- else Failed
- }
-
- case object Ok extends Status("ok")
- case object Skipped extends Status("skipped")
- case object Failed extends Status("failed")
+ 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 */
- private def compute_timing(results: Build.Results, group: Option[String]): Timing = {
- val timings =
- results.sessions.collect {
- case session if group.forall(results.info(session).groups.contains(_)) =>
- results(session).timing
- }
- timings.foldLeft(Timing.zero)(_ + _)
- }
+ 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()
- private def with_documents(options: Options, config: Build_Config): Options = {
- if (config.documents) {
- options + "browser_info" + "document=pdf" + "document_variants=document:outline=/proof,/ML"
- }
- else options
- }
-
- def hg_id(path: Path): String =
- if (Mercurial.Hg_Sync.ok(path)) File.read(path + Mercurial.Hg_Sync.PATH_ID)
- else Mercurial.repository(path).id()
-
- def print_section(title: String): Unit =
- println("\n=== " + title + " ===\n")
-
- def ci_build(options: Options, build_hosts: List[Build_Cluster.Host], job: Job): Unit = {
- val hosts = job.hosts
- val config = job.config
-
- val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
- val isabelle_id = hg_id(isabelle_home)
+ 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 start_time = Time.now()
- val formatted_time = start_time.instant.atZone(ZoneId.systemDefault).format(
- DateTimeFormatter.RFC_1123_DATE_TIME)
-
- print_section("CONFIGURATION")
- println(Build_Log.Settings.show())
+ val mail_result =
+ return_code {
+ Mail_System.try_open(options).getOrElse(error("No mail configuration")).server.check()
+ }
- val build_options = with_documents(options, config) + "parallel_proofs=1" + "system_heaps"
-
- println(hosts)
-
- print_section("BUILD")
- println("Build started at " + formatted_time)
- println("Isabelle id " + isabelle_id)
- val pre_result = config.pre_hook(options)
+ val pre_result = return_code { job.hook.pre(options, progress) }
- print_section("LOG")
- val (results, elapsed_time) = {
- val progress = new Console_Progress(verbose = true)
- val start_time = Time.now()
- val results = progress.interrupt_handler {
- Build.build(
- build_options ++ hosts.prefs,
- build_hosts = build_hosts,
- selection = config.selection,
- progress = progress,
- clean_build = config.clean,
- numa_shuffling = hosts.numa_shuffling,
- max_jobs = hosts.max_jobs,
- dirs = config.include,
- select_dirs = config.select)
- }
- val end_time = Time.now()
- (results, end_time - start_time)
+ 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)
}
- print_section("TIMING")
+ val post_result = return_code { job.hook.post(options, start_date, url, results, progress) }
- val groups = results.sessions.map(results.info).flatMap(_.groups)
- for (group <- groups)
- println("Group " + group + ": " + compute_timing(results, Some(group)).message_resources)
+ val rc = List(mail_result, pre_result, results.rc, post_result).max
+ if (rc != Process_Result.RC.ok) {
+ progress.echo(section("FAILED"))
- val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
- println("Overall: " + total_timing.message_resources)
+ 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 (!results.ok) {
- print_section("FAILED SESSIONS")
-
+ if (pre_result != Process_Result.RC.ok) progress.echo("Pre-hook: FAILED")
for (name <- results.sessions) {
- if (results.cancelled(name)) println("Session " + name + ": CANCELLED")
+ if (results.cancelled(name)) progress.echo("Session " + name + ": CANCELLED")
else {
val result = results(name)
- if (!result.ok) println("Session " + name + ": FAILED " + result.rc)
+ if (!result.ok) progress.echo("Session " + name + ": FAILED " + result.rc)
}
}
+ if (post_result != Process_Result.RC.ok) progress.echo("Post-hook: FAILED")
}
- val post_result = config.post_hook(results, options, start_time)
-
- sys.exit(List(pre_result.rc, results.rc, post_result.rc).max)
+ sys.exit(rc)
}
@@ -246,10 +226,9 @@
val isabelle_tool = Isabelle_Tool("ci_build", "builds Isabelle jobs in ci environments",
Scala_Project.here,
{ args =>
- /* arguments */
-
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
@@ -257,6 +236,7 @@
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).
@@ -264,20 +244,24 @@
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),
- "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.load(Nil), 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 job =
+ more_args match {
+ case job :: Nil => the_job(job)
+ case _ => getopts.usage()
+ }
- ci_build(options, build_hosts.toList, job)
+ val progress = new Console_Progress(verbose = true)
+
+ ci_build(options, job, url = url, build_hosts = build_hosts.toList, progress = progress)
})
}
-class Isabelle_CI_Builds(val jobs: CI_Build.Job*) extends Isabelle_System.Service
+class Isabelle_CI_Jobs(val jobs: CI_Build.Job*) extends Isabelle_System.Service
-class CI_Builds extends Isabelle_CI_Builds(CI_Build.timing)
+class CI_Jobs extends Isabelle_CI_Jobs(CI_Build.timing)