diff -r 906a7684fdce -r a9fce67fb8b2 src/Pure/Admin/ci_build.scala --- 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)