# HG changeset patch # User wenzelm # Date 1719601317 -7200 # Node ID cba532bf431627dd4356c2b1907b9c6b7c926528 # Parent 6ed82923d51df96d4022b8b544cae7dfe9a2f130# Parent acbd22e7e3ecf9c6c75eb54695340587ef7d5a40 merged diff -r acbd22e7e3ec -r cba532bf4316 Admin/etc/settings --- a/Admin/etc/settings Fri Jun 28 18:30:26 2024 +0200 +++ b/Admin/etc/settings Fri Jun 28 21:01:57 2024 +0200 @@ -1,5 +1,3 @@ # -*- shell-script -*- :mode=shellscript: ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" - -ISABELLE_JENKINS_ROOT="https://ci.isabelle.systems/jenkins" diff -r acbd22e7e3ec -r cba532bf4316 Admin/jenkins/build/etc/settings --- a/Admin/jenkins/build/etc/settings Fri Jun 28 18:30:26 2024 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2 +0,0 @@ -ISABELLE_TOOLS="$COMPONENT:$ISABELLE_TOOLS" -ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g" diff -r acbd22e7e3ec -r cba532bf4316 Admin/jenkins/run_build --- a/Admin/jenkins/run_build Fri Jun 28 18:30:26 2024 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -#!/usr/bin/env bash -# -# Do not run this script manually, it is only to be executed by Jenkins. - -set -x -set -e - -PROFILE="$1" -shift - -bin/isabelle components -a -bin/isabelle jedit -bf -bin/isabelle ocaml_setup -bin/isabelle ghc_setup -bin/isabelle go_setup -bin/isabelle ci_build "$PROFILE" "$@" diff -r acbd22e7e3ec -r cba532bf4316 etc/build.props --- a/etc/build.props Fri Jun 28 18:30:26 2024 +0200 +++ b/etc/build.props Fri Jun 28 21:01:57 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 \ @@ -332,7 +332,7 @@ isabelle.Bibtex$File_Format \ isabelle.Build$Engine$Default \ isabelle.Build_Schedule$Build_Engine \ - isabelle.CI_Builds \ + isabelle.CI_Jobs \ isabelle.Document_Build$Build_Engine \ isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \ isabelle.Document_Build$LIPIcs_PDFLaTeX_Engine \ diff -r acbd22e7e3ec -r cba532bf4316 etc/options --- a/etc/options Fri Jun 28 18:30:26 2024 +0200 +++ b/etc/options Fri Jun 28 21:01:57 2024 +0200 @@ -512,3 +512,9 @@ option ci_mail_sender : string = "" for connection option ci_mail_smtp_host : string = "" for connection option ci_mail_smtp_port : int = 587 for connection + +option ci_mail_from : string = "ci@isabelle.systems" + -- "mail address for build failure notifications" + +option ci_mail_to : string = "" + -- "recipient address for build failure notifications" diff -r acbd22e7e3ec -r cba532bf4316 src/HOL/List.thy --- a/src/HOL/List.thy Fri Jun 28 18:30:26 2024 +0200 +++ b/src/HOL/List.thy Fri Jun 28 21:01:57 2024 +0200 @@ -182,7 +182,7 @@ "find P (x#xs) = (if P x then Some x else find P xs)" text \In the context of multisets, \count_list\ is equivalent to - \<^term>\count \ mset\ and it it advisable to use the latter.\ + \<^term>\count \ mset\ and it is advisable to use the latter.\ primrec count_list :: "'a list \ 'a \ nat" where "count_list [] y = 0" | "count_list (x#xs) y = (if x=y then count_list xs y + 1 else count_list xs y)" diff -r acbd22e7e3ec -r cba532bf4316 src/Pure/Admin/ci_build.scala --- a/src/Pure/Admin/ci_build.scala Fri Jun 28 18:30:26 2024 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,283 +0,0 @@ -/* Title: Pure/Admin/ci_build.scala - Author: Lars Hupel and Fabian Huch, TU Munich - -Build profile for continuous integration services. -*/ - -package isabelle - - -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 */ - - case class Result(rc: Int) - case object Result { - def ok: Result = Result(Process_Result.RC.ok) - def error: Result = Result(Process_Result.RC.error) - } - - - /* 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 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 - } - - 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 - - sealed case class Job( - name: String, - description: String, - hosts: Hosts, - config: Build_Config, - components: List[String] = Nil, - trigger: Trigger = On_Commit - ) { - 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", - 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 */ - - 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 = - 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) - - 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) + "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) - - 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) - } - - print_section("TIMING") - - val groups = results.sessions.map(results.info).flatMap(_.groups) - for (group <- groups) - 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("Session " + name + ": CANCELLED") - else { - val result = results(name) - 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 build_hosts = new mutable.ListBuffer[Build_Cluster.Host] - - 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) - - 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", - "o:" -> (arg => options = options + arg), - "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.load(Nil), arg))) - - val more_args = getopts(args) - - val job = more_args match { - case job :: Nil => the_job(job) - case _ => getopts.usage() - } - - ci_build(options, build_hosts.toList, job) - }) -} - -class Isabelle_CI_Builds(val jobs: CI_Build.Job*) extends Isabelle_System.Service - -class CI_Builds extends Isabelle_CI_Builds(CI_Build.timing) diff -r acbd22e7e3ec -r cba532bf4316 src/Pure/Build/build_ci.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Build/build_ci.scala Fri Jun 28 21:01:57 2024 +0200 @@ -0,0 +1,275 @@ +/* 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, + 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, + other_settings: 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 = { + 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 stop_date = progress.now() + val elapsed_time = stop_date - progress.start + progress.echo("\nFinished at " + Build_Log.print_date(stop_date)) + + progress.echo(section("TIMING")) + val total_timing = + results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _). + copy(elapsed = elapsed_time) + progress.echo(total_timing.message_resources) + + val post_result = return_code { job.hook.post(options, 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) diff -r acbd22e7e3ec -r cba532bf4316 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Fri Jun 28 18:30:26 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Fri Jun 28 21:01:57 2024 +0200 @@ -35,19 +35,24 @@ def components: List[Component] def fresh_build: Boolean def build_cluster: Boolean - def command(build_hosts: List[Build_Cluster.Host]): String + def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String } 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"))) + + def task(job: Build_CI.Job): Task = + Task(CI_Build(job), job.hosts.hosts_spec, other_settings = job.other_settings, + isabelle_rev = "default") } case class CI_Build(name: String, build_cluster: Boolean, components: List[Component]) extends Build_Config { def fresh_build: Boolean = true - def command(build_hosts: List[Build_Cluster.Host]): String = - " ci_build" + + def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = + " build_ci" + + " -u " + Bash.string(job_url.toString) + if_proper(build_cluster, build_hosts.map(host => " -H " + Bash.string(host.print)).mkString) + " " + name } @@ -76,20 +81,23 @@ def name: String = User_Build.name def components: List[Component] = afp_rev.map(Component.AFP).toList def build_cluster: Boolean = true - def command(build_hosts: List[Build_Cluster.Host]): String = { + def command(job_url: Url, build_hosts: List[Build_Cluster.Host]): String = { " build" + if_proper(afp_rev, " -A:") + base_sessions.map(session => " -B " + Bash.string(session)).mkString + build_hosts.map(host => " -H " + Bash.string(host.print)).mkString + if_proper(presentation, " -P:") + if_proper(requirements, " -R") + + exclude_session_groups.map(session => " -X " + Bash.string(session)).mkString + if_proper(all_sessions, " -a") + if_proper(build_heap, " -b") + if_proper(clean_build, " -c") + if_proper(export_files, " -e") + if_proper(fresh_build, " -f") + + session_groups.map(session => " -g " + Bash.string(session)).mkString + Options.Spec.bash_strings(prefs, bg = true) + if_proper(verbose, " -v") + + exclude_sessions.map(session => " -x " + Bash.string(session)).mkString + sessions.map(session => " " + Bash.string(session)).mkString } } @@ -105,6 +113,7 @@ sealed case class Task( build_config: Build_Config, hosts_spec: String, + other_settings: List[String] = Nil, uuid: UUID.T = UUID.random(), submit_date: Date = Date.now(), priority: Priority = Priority.normal, @@ -317,6 +326,7 @@ val kind = SQL.Column.string("kind") val build_cluster = SQL.Column.bool("build_cluster") val hosts_spec = SQL.Column.string("hosts_spec") + val other_settings = SQL.Column.string("other_settings") val uuid = SQL.Column.string("uuid").make_primary_key val submit_date = SQL.Column.date("submit_date") val priority = SQL.Column.string("priority") @@ -339,10 +349,10 @@ val verbose = SQL.Column.bool("verbose") val table = - make_table(List(kind, build_cluster, hosts_spec, uuid, submit_date, priority, isabelle_rev, - components, prefs, requirements, all_sessions, base_sessions, exclude_session_groups, - exclude_sessions, session_groups, sessions, build_heap, clean_build, export_files, - fresh_build, presentation, verbose), + make_table(List(kind, build_cluster, hosts_spec, other_settings, uuid, submit_date, + priority, isabelle_rev, components, prefs, requirements, all_sessions, base_sessions, + exclude_session_groups, exclude_sessions, session_groups, sessions, build_heap, + clean_build, export_files, fresh_build, presentation, verbose), name = "pending") } @@ -352,6 +362,7 @@ val kind = res.string(Pending.kind) val build_cluster = res.bool(Pending.build_cluster) val hosts_spec = res.string(Pending.hosts_spec) + val other_settings = split_lines(res.string(Pending.other_settings)) val uuid = res.string(Pending.uuid) val submit_date = res.date(Pending.submit_date) val priority = Priority.valueOf(res.string(Pending.priority)) @@ -383,8 +394,8 @@ clean_build, export_files, fresh_build, presentation, verbose) } - val task = - Task(build_config, hosts_spec, UUID.make(uuid), submit_date, priority, isabelle_rev) + val task = Task(build_config, hosts_spec, other_settings, UUID.make(uuid), submit_date, + priority, isabelle_rev) task.name -> task }) @@ -407,11 +418,12 @@ stmt.string(1) = task.kind stmt.bool(2) = task.build_cluster stmt.string(3) = task.hosts_spec - stmt.string(4) = task.uuid.toString - stmt.date(5) = task.submit_date - stmt.string(6) = task.priority.toString - stmt.string(7) = task.isabelle_rev - stmt.string(8) = task.components.mkString(",") + stmt.string(4) = cat_lines(task.other_settings) + stmt.string(5) = task.uuid.toString + stmt.date(6) = task.submit_date + stmt.string(7) = task.priority.toString + stmt.string(8) = task.isabelle_rev + stmt.string(9) = task.components.mkString(",") def get[A](f: User_Build => A): Option[A] = task.build_config match { @@ -419,20 +431,20 @@ case _ => None } - stmt.string(9) = get(user_build => user_build.prefs.map(_.print).mkString(",")) - stmt.bool(10) = get(_.requirements) - stmt.bool(11) = get(_.all_sessions) - stmt.string(12) = get(_.base_sessions.mkString(",")) - stmt.string(13) = get(_.exclude_session_groups.mkString(",")) - stmt.string(14) = get(_.exclude_sessions.mkString(",")) - stmt.string(15) = get(_.session_groups.mkString(",")) - stmt.string(16) = get(_.sessions.mkString(",")) - stmt.bool(17) = get(_.build_heap) - stmt.bool(18) = get(_.clean_build) - stmt.bool(19) = get(_.export_files) - stmt.bool(20) = get(_.fresh_build) - stmt.bool(21) = get(_.presentation) - stmt.bool(22) = get(_.verbose) + stmt.string(10) = get(user_build => user_build.prefs.map(_.print).mkString(",")) + stmt.bool(11) = get(_.requirements) + stmt.bool(12) = get(_.all_sessions) + stmt.string(13) = get(_.base_sessions.mkString(",")) + stmt.string(14) = get(_.exclude_session_groups.mkString(",")) + stmt.string(15) = get(_.exclude_sessions.mkString(",")) + stmt.string(16) = get(_.session_groups.mkString(",")) + stmt.string(17) = get(_.sessions.mkString(",")) + stmt.bool(18) = get(_.build_heap) + stmt.bool(19) = get(_.clean_build) + stmt.bool(20) = get(_.export_files) + stmt.bool(21) = get(_.fresh_build) + stmt.bool(22) = get(_.presentation) + stmt.bool(23) = get(_.verbose) }) } @@ -727,6 +739,11 @@ private def start_next(): Option[Context] = synchronized_database("start_next") { + for ((name, task) <- _state.pending if Exn.is_exn(Exn.capture(task.build_hosts))) { + progress.echo("Invalid host spec for task " + name + ": " + quote(task.hosts_spec)) + _state = _state.remove_pending(name) + } + _state.next(build_hosts).flatMap { task => echo("Initializing " + task.name) @@ -850,7 +867,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], @@ -880,14 +897,10 @@ 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) - } { - val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, priority = Priority.low, - isabelle_rev = "default") - _state = _state.add_pending(task) - } + } _state = _state.add_pending(CI_Build.task(ci_job)) } } @@ -909,7 +922,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], @@ -921,8 +934,8 @@ 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) => - val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, isabelle_rev = "default") + case Build_CI.Timed(in_interval) if in_interval(previous, next) => + val task = CI_Build.task(ci_job) echo("Triggered task " + task.kind) _state = _state.add_pending(task) case _ => @@ -1022,6 +1035,13 @@ main(chapter(name) :: body ::: Nil) :: Nil } + private def summary(start: Date): XML.Body = + text(" running since " + Build_Log.print_date(start)) + + private def summary(status: Status, start: Date, end: Option[Date]): XML.Body = + text(" (" + status.toString + if_proper(end, " in " + (end.get - start).message_hms) + + ") on " + Build_Log.print_date(start)) + def render_home(state: State): XML.Body = render_page("Dashboard") { def render_kind(kind: String): XML.Elem = { val running = state.get_running(kind).sortBy(_.id).reverse @@ -1031,18 +1051,17 @@ val (failed, rest) = finished.span(_.status != Status.ok) val first_failed = failed.lastOption.map(result => par( - text("first failure: ") ::: - link_build(result.name, result.id) :: - text(" on " + result.start_date))) + text("first failure: ") ::: link_build(result.name, result.id) :: + summary(result.status, result.start_date, result.end_date))) val last_success = rest.headOption.map(result => par( text("last success: ") ::: link_build(result.name, result.id) :: - text(" on " + result.start_date))) + summary(result.status, result.start_date, result.end_date))) first_failed.toList ::: last_success.toList } def render_job(job: Job): XML.Body = - par(link_build(job.name, job.id) :: text(": running since " + job.start_date)) :: + par(link_build(job.name, job.id) :: summary(job.start_date)) :: render_if( finished.headOption.exists(_.status != Status.ok) && job.kind != User_Build.name, render_previous(finished)) @@ -1050,7 +1069,7 @@ def render_result(result: Result): XML.Body = par( link_build(result.name, result.id) :: - text(" (" + result.status.toString + ") on " + result.start_date)) :: + summary(result.status, result.start_date, result.end_date)) :: render_if(result.status != Status.ok && result.kind != User_Build.name, render_previous(finished.tail)) @@ -1063,18 +1082,18 @@ text("Queue: " + state.pending.size + " tasks waiting") ::: section("Builds") :: par(text("Total: " + state.num_builds + " builds")) :: - state.kinds.map(render_kind) + state.kinds.sorted.map(render_kind) } def render_overview(kind: String, state: State): XML.Body = render_page("Overview: " + kind + " job ") { def render_job(job: Job): XML.Body = - List(par(link_build(job.name, job.id) :: text(" running since " + job.start_date))) + List(par(link_build(job.name, job.id) :: summary(job.start_date))) def render_result(result: Result): XML.Body = List(par( link_build(result.name, result.id) :: - text(" (" + result.status + ") on " + result.start_date))) + summary(result.status, result.start_date, result.end_date))) itemize( state.get_running(kind).sortBy(_.id).reverse.map(render_job) ::: @@ -1098,18 +1117,20 @@ build match { case task: Task => - par(text("Task from " + task.submit_date + ". ")) :: + par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) :: render_rev(task.isabelle_rev, task.components) ::: render_cancel(task.uuid) case job: Job => - par(text("Start: " + job.start_date)) :: + par(text("Start: " + Build_Log.print_date(job.start_date))) :: par( if (job.cancelled) text("Cancelling...") else text("Running...") ::: render_cancel(job.uuid)) :: render_rev(job.isabelle_rev, job.components) ::: source(cache.lookup(store, job.kind, job.id)) :: Nil case result: Result => - par(text("Date: " + result.start_date)) :: + par(text("Start: " + Build_Log.print_date(result.start_date) + + if_proper(result.end_date, + ", took " + (result.end_date.get - result.start_date).message_hms))) :: par(text("Status: " + result.status)) :: source(cache.lookup(store, result.kind, result.id)) :: Nil } @@ -1256,10 +1277,12 @@ } yield "init_component " + quote(target.absolute.implode) _isabelle.init( - other_settings = _isabelle.init_components() ::: init_components, + other_settings = _isabelle.init_components() ::: init_components ::: task.other_settings, fresh = task.build_config.fresh_build, echo = true) - val cmd = task.build_config.command(task.build_hosts) + val paths = Web_Server.paths(context.store) + val job_url = paths.frontend_url(Web_Server.Page.BUILD, Markup.Name(context.name)) + val cmd = task.build_config.command(job_url, task.build_hosts) progress.echo("isabelle" + cmd) val script = File.bash_path(Isabelle_Tool.exe(_isabelle.isabelle_home)) + cmd @@ -1351,8 +1374,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))) @@ -1528,7 +1550,7 @@ val build_config = User_Build(afp_rev, prefs, requirements, all_sessions, base_sessions, exclude_session_groups, exclude_sessions, session_groups, sessions, build_heap, clean_build, export_files, fresh_build, presentation, verbose) - val task = Task(build_config, hosts_spec, uuid, Date.now(), Priority.high) + val task = Task(build_config, hosts_spec, uuid = uuid, priority = Priority.high) val dir = store.task_dir(task) @@ -1583,7 +1605,7 @@ var fresh_build = false val session_groups = new mutable.ListBuffer[String] var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS) - var prefs: List[Options.Spec] = Nil + val prefs = new mutable.ListBuffer[Options.Spec] var verbose = false var rev = "" val exclude_sessions = new mutable.ListBuffer[String] @@ -1604,7 +1626,7 @@ -f fresh build -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -p OPTIONS comma-separated preferences for build process + -p OPTION override Isabelle system OPTION for build process (via NAME=VAL or NAME) -r REV explicit revision (default: state of working directory) -v verbose -x NAME exclude session NAME and all descendants @@ -1624,7 +1646,7 @@ "f" -> (_ => fresh_build = true), "g:" -> (arg => session_groups += arg), "o:" -> (arg => options = options + arg), - "p:" -> (arg => prefs = Options.Spec.parse(arg)), + "p:" -> (arg => prefs += Options.Spec.make(arg)), "r:" -> (arg => rev = arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions += arg)) @@ -1638,7 +1660,7 @@ exclude_session_groups = exclude_session_groups.toList, all_sessions = all_sessions, build_heap = build_heap, clean_build = clean_build, export_files = export_files, fresh_build = fresh_build, session_groups = session_groups.toList, sessions = sessions, - prefs = prefs, verbose = verbose, rev = rev, exclude_sessions = exclude_sessions.toList, - progress = progress) + prefs = prefs.toList, verbose = verbose, rev = rev, exclude_sessions = + exclude_sessions.toList, progress = progress) }) } diff -r acbd22e7e3ec -r cba532bf4316 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri Jun 28 18:30:26 2024 +0200 +++ b/src/Pure/System/isabelle_tool.scala Fri Jun 28 21:01:57 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,