# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1664452706 -7200
# Node ID 3c4e373922ca69b92d43188c04d47a2e6f538dc1
# Parent  1f2e78b7df933ed17d934f08382da2ef78c181e1
restructured ci profile into modular ci build system;

diff -r 1f2e78b7df93 -r 3c4e373922ca Admin/jenkins/run_build
--- 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" "$@"
diff -r 1f2e78b7df93 -r 3c4e373922ca etc/build.props
--- 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 \
diff -r 1f2e78b7df93 -r 3c4e373922ca src/Pure/Admin/ci_build.scala
--- /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)
diff -r 1f2e78b7df93 -r 3c4e373922ca src/Pure/Admin/ci_build_benchmark.scala
--- 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)
-  })
-}
diff -r 1f2e78b7df93 -r 3c4e373922ca src/Pure/Admin/ci_profile.scala
--- 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
diff -r 1f2e78b7df93 -r 3c4e373922ca src/Pure/System/isabelle_tool.scala
--- 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,