--- 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"
--- 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"
--- 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" "$@"
--- 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 \
--- 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"
--- 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 \<open>In the context of multisets, \<open>count_list\<close> is equivalent to
- \<^term>\<open>count \<circ> mset\<close> and it it advisable to use the latter.\<close>
+ \<^term>\<open>count \<circ> mset\<close> and it is advisable to use the latter.\<close>
primrec count_list :: "'a list \<Rightarrow> 'a \<Rightarrow> 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)"
--- 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)
--- /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)
--- 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)
})
}
--- 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,