diff --git a/src/Pure/Admin/ci_build.scala b/src/Pure/Admin/ci_build.scala --- a/src/Pure/Admin/ci_build.scala +++ b/src/Pure/Admin/ci_build.scala @@ -1,245 +1,246 @@ /* Title: Pure/Admin/ci_build.scala Author: Lars Hupel and Fabian Huch, TU Munich Build profile for continuous integration services. */ package isabelle 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 */ case class Result(rc: Int) case object Result { def ok: Result = Result(Process_Result.RC.ok) def error: Result = Result(Process_Result.RC.error) } /* executor profile */ case class Profile(threads: Int, jobs: Int, numa: Boolean) object Profile { def from_host: Profile = { Isabelle_System.hostname() match { case "hpcisabelle" => Profile(8, 8, numa = true) case "lxcisa1" => Profile(4, 10, numa = false) case _ => Profile(2, 2, numa = false) } } } /* 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) 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 */ sealed case class Job(name: String, description: String, profile: Profile, config: Build_Config) { override def toString: String = name } private lazy val known_jobs: List[Job] = Isabelle_System.make_services(classOf[Isabelle_CI_Builds]).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)) val timing = Job( "benchmark", "runs benchmark and timing sessions", Profile(threads = 6, jobs = 1, numa = false), Build_Config( documents = false, select = List( Path.explode("$ISABELLE_HOME/src/Benchmarks")), selection = Sessions.Selection(session_groups = List("timing")))) /* session status */ 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") /* 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)(_ + _) } 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 = Mercurial.repository(path).id() def print_section(title: String): Unit = - println(s"\n=== $title ===\n") + println("\n=== " + title + " ===\n") def ci_build(options: Options, job: Job): Unit = { val profile = job.profile val config = job.config val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) val isabelle_id = hg_id(isabelle_home) 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 build_options = with_documents(options, config).int.update("threads", profile.threads) + "parallel_proofs=1" + "system_heaps" - println(s"jobs = ${profile.jobs}, threads = ${profile.threads}, numa = ${profile.numa}") + println( + "jobs = " + profile.jobs + ", threads = " + profile.threads + ", numa = " + profile.numa) print_section("BUILD") - println(s"Build started at $formatted_time") - println(s"Isabelle id $isabelle_id") + println("Build started at " + formatted_time) + println("Isabelle id " + isabelle_id) val pre_result = config.pre_hook(options) 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, selection = config.selection, progress = progress, clean_build = config.clean, numa_shuffling = profile.numa, max_jobs = Some(profile.jobs), dirs = config.include, select_dirs = config.select) } val end_time = Time.now() (results, end_time - start_time) } print_section("TIMING") val groups = results.sessions.map(results.info).flatMap(_.groups) for (group <- groups) - println(s"Group $group: " + compute_timing(results, Some(group)).message_resources) + println("Group " + group + ": " + compute_timing(results, Some(group)).message_resources) val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time) println("Overall: " + total_timing.message_resources) if (!results.ok) { print_section("FAILED SESSIONS") for (name <- results.sessions) { - if (results.cancelled(name)) println(s"Session $name: CANCELLED") + if (results.cancelled(name)) println("Session " + name + ": CANCELLED") else { val result = results(name) - if (!result.ok) println(s"Session $name: FAILED ${ result.rc }") + if (!result.ok) println("Session " + name + ": FAILED " + result.rc) } } } val post_result = config.post_hook(results, options, start_time) sys.exit(List(pre_result.rc, results.rc, post_result.rc).max) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("ci_build", "builds Isabelle jobs in ci environments", Scala_Project.here, { args => /* arguments */ var options = Options.init() val getopts = Getopts(""" Usage: isabelle ci_build [OPTIONS] JOB Options are: -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Runs Isabelle builds in ci environment, with the following build jobs: """ + Library.indent_lines(4, show_jobs) + "\n", "o:" -> (arg => options = options + arg)) val more_args = getopts(args) val job = more_args match { case job :: Nil => the_job(job) case _ => getopts.usage() } ci_build(options, job) }) } class Isabelle_CI_Builds(val jobs: CI_Build.Job*) extends Isabelle_System.Service class CI_Builds extends Isabelle_CI_Builds(CI_Build.timing)