src/Pure/Admin/ci_profile.scala

proper replacement for (map_types (K dummyT));

/*  Title:      Pure/Admin/ci_profile.scala
    Author:     Lars Hupel

Build profile for continuous integration services.
*/

package isabelle


import java.time.{Instant, ZoneId}
import java.time.format.DateTimeFormatter
import java.util.{Properties => JProperties, Map => JMap}


abstract class CI_Profile extends Isabelle_Tool.Body
{
  private def build(options: Options): (Build.Results, Time) =
  {
    val progress = new Console_Progress(verbose = true)
    val start_time = Time.now()
    val results = progress.interrupt_handler {
      Build.build(
        options = options + "system_heaps",
        progress = progress,
        clean_build = clean,
        verbose = true,
        numa_shuffling = numa,
        max_jobs = jobs,
        dirs = include,
        select_dirs = select,
        selection = selection)
    }
    val end_time = Time.now()
    (results, end_time - start_time)
  }

  private def load_properties(): JProperties =
  {
    val props = new JProperties()
    val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")

    if (file_name != "")
    {
      val file = Path.explode(file_name).file
      if (file.exists())
        props.load(new java.io.FileReader(file))
      props
    }
    else
      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
    }
    (Timing.zero /: timings)(_ + _)
  }

  private def with_documents(options: Options): Options =
  {
    if (documents)
      options
        .bool.update("browser_info", true)
        .string.update("document", "pdf")
        .string.update("document_variants", "document:outline=/proof,/ML")
    else
      options
  }


  final def hg_id(path: Path): String =
    Mercurial.repository(path).id()

  final def print_section(title: String): Unit =
    println(s"\n=== $title ===\n")


  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
  final val isabelle_id = hg_id(isabelle_home)
  final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)


  override final def apply(args: List[String]): Unit =
  {
    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())
        .int.update("parallel_proofs", 1)
        .int.update("threads", threads)

    println(s"jobs = $jobs, threads = $threads, numa = $numa")

    print_section("BUILD")
    println(s"Build started at $start_time")
    println(s"Isabelle id $isabelle_id")
    pre_hook(args)

    print_section("LOG")
    val (results, elapsed_time) = build(options)

    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}")
        }
      }
    }

    post_hook(results)

    System.exit(results.rc)
  }

  /* profile */

  def threads: Int = Isabelle_System.hostname() match {
    case "hpcisabelle" => 8
    case "lxcisa1" => 4
    case _ => 2
  }

  def jobs: Int = Isabelle_System.hostname() match {
    case "hpcisabelle" => 8
    case "lxcisa1" => 10
    case _ => 2
  }

  def numa: Boolean = Isabelle_System.hostname() == "hpcisabelle"

  def documents: Boolean = true
  def clean: Boolean = true

  def include: List[Path]
  def select: List[Path]

  def pre_hook(args: List[String]): Unit
  def post_hook(results: Build.Results): Unit

  def selection: Sessions.Selection
}