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,244 +1,244 @@ /* Title: Pure/Admin/ci_profile.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: () => Result = () => Result.ok, post_hook: (Build.Results, Time) => Result = (_, _) => Result.ok, selection: Sessions.Selection = Sessions.Selection.empty ) /* 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)) + error("Unknown job " + quote(name)) val timing = Job( - "timing", "runs benchmark and timing sessions", + "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 load_properties(): JProperties = { val props = new JProperties val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") if (file_name.nonEmpty) { val path = Path.explode(file_name) if (path.is_file) props.load(Files.newBufferedReader(path.java_path)) } props } 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 .bool.update("browser_info", true) .string.update("document", "pdf") .string.update("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") def ci_build(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 props = load_properties() System.getProperties.asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props) val options = with_documents(Options.init(), config) .int.update("parallel_proofs", 1) .int.update("threads", profile.threads) println(s"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") val pre_result = config.pre_hook() 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( options + "system_heaps", selection = config.selection, progress = progress, clean_build = config.clean, verbose = true, numa_shuffling = profile.numa, max_jobs = 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) 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") else { val result = results(name) if (!result.ok) println(s"Session $name: FAILED ${ result.rc }") } } } val post_result = config.post_hook(results, 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 => val getopts = Getopts(""" Usage: isabelle ci_build [JOB] Runs Isabelle builds in ci environment, with the following build jobs: """ + Library.indent_lines(4, show_jobs) + "\n") val more_args = getopts(args) val job = more_args match { case job :: Nil => the_job(job) case _ => getopts.usage() } ci_build(job) }) } class Isabelle_CI_Builds(val jobs: CI_Build.Job*) extends Isabelle_System.Service class CI_Builds extends Isabelle_CI_Builds(CI_Build.timing)