--- a/Admin/jenkins/run_build Wed Sep 28 19:14:57 2022 +0100
+++ b/Admin/jenkins/run_build Thu Sep 29 13:58:26 2022 +0200
@@ -12,4 +12,4 @@
bin/isabelle jedit -bf
bin/isabelle ocaml_setup
bin/isabelle ghc_setup
-bin/isabelle "ci_build_$PROFILE" "$@"
+bin/isabelle "ci_build $PROFILE" "$@"
--- a/etc/build.props Wed Sep 28 19:14:57 2022 +0100
+++ b/etc/build.props Thu Sep 29 13:58:26 2022 +0200
@@ -35,8 +35,7 @@
src/Pure/Admin/build_verit.scala \
src/Pure/Admin/build_zipperposition.scala \
src/Pure/Admin/check_sources.scala \
- src/Pure/Admin/ci_build_benchmark.scala \
- src/Pure/Admin/ci_profile.scala \
+ src/Pure/Admin/ci_build.scala \
src/Pure/Admin/isabelle_cronjob.scala \
src/Pure/Admin/isabelle_devel.scala \
src/Pure/Admin/jenkins.scala \
@@ -295,6 +294,7 @@
isabelle.Document_Build$Build_Engine \
isabelle.Document_Build$LuaLaTeX_Engine \
isabelle.Document_Build$PDFLaTeX_Engine \
+ isabelle.CI_Builds \
isabelle.ML_Statistics$Handler \
isabelle.Print_Operation$Handler \
isabelle.Scala$Handler \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/ci_build.scala Thu Sep 29 13:58:26 2022 +0200
@@ -0,0 +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))
+
+ val timing =
+ Job(
+ "timing", "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)
--- a/src/Pure/Admin/ci_build_benchmark.scala Wed Sep 28 19:14:57 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-/* Title: Pure/Admin/ci_build_benchmark.scala
- Author: Lars Hupel and Fabian Huch, TU Munich
-
-CI benchmark build profile.
-*/
-
-package isabelle
-
-
-object CI_Build_Benchmark {
- val isabelle_tool =
- Isabelle_Tool("ci_build_benchmark", "builds Isabelle benchmarks + timing group",
- Scala_Project.here, { args =>
- val getopts = Getopts("""
-Usage: isabelle ci_build_benchmark
-
- Builds Isabelle benchmark and timing sessions.
- """)
- getopts(args)
-
- val selection = Sessions.Selection(session_groups = List("timing"))
- val profile = CI_Profile.Profile(threads = 6, jobs = 1, numa = false)
- val config = CI_Profile.Build_Config(documents = false,
- select = List(Path.explode("$ISABELLE_HOME/src/Benchmarks")), selection = selection)
-
- CI_Profile.build(profile, config)
- })
-}
--- a/src/Pure/Admin/ci_profile.scala Wed Sep 28 19:14:57 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,184 +0,0 @@
-/* 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.format.DateTimeFormatter
-import java.util.{Properties => JProperties, Map => JMap}
-import java.nio.file.Files
-
-
-object CI_Profile {
-
- /* 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)
- }
-
-
- /* 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 => Result = _ => Result.ok,
- selection: Sessions.Selection = Sessions.Selection.empty
- )
-
-
- /* 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")
-
-
- 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 build(profile: Profile, config: Build_Config): Unit = {
- val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
- val isabelle_id = hg_id(isabelle_home)
-
- val start_time =
- Date.Format.make(List(DateTimeFormatter.RFC_1123_DATE_TIME))(Date.now())
-
- 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 $start_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)
-
- sys.exit(List(pre_result.rc, results.rc, post_result.rc).max)
- }
-}
\ No newline at end of file
--- a/src/Pure/System/isabelle_tool.scala Wed Sep 28 19:14:57 2022 +0100
+++ b/src/Pure/System/isabelle_tool.scala Thu Sep 29 13:58:26 2022 +0200
@@ -123,7 +123,7 @@
Build.isabelle_tool,
Build_Docker.isabelle_tool,
Build_Job.isabelle_tool,
- CI_Build_Benchmark.isabelle_tool,
+ CI_Build.isabelle_tool,
Doc.isabelle_tool,
Document_Build.isabelle_tool,
Dump.isabelle_tool,