1/*  Title:      Pure/Admin/ci_profile.scala
2    Author:     Lars Hupel
3
4Build profile for continuous integration services.
5*/
6
7package isabelle
8
9
10import java.time.{Instant, ZoneId}
11import java.time.format.DateTimeFormatter
12import java.util.{Properties => JProperties, Map => JMap}
13
14
15abstract class CI_Profile extends Isabelle_Tool.Body
16{
17  private def build(options: Options): (Build.Results, Time) =
18  {
19    val progress = new Console_Progress(verbose = true)
20    val start_time = Time.now()
21    val results = progress.interrupt_handler {
22      Build.build(
23        options = options,
24        progress = progress,
25        clean_build = clean,
26        verbose = true,
27        numa_shuffling = numa,
28        max_jobs = jobs,
29        dirs = include,
30        select_dirs = select,
31        system_mode = true,
32        selection = selection)
33    }
34    val end_time = Time.now()
35    (results, end_time - start_time)
36  }
37
38  private def load_properties(): JProperties =
39  {
40    val props = new JProperties()
41    val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
42
43    if (file_name != "")
44    {
45      val file = Path.explode(file_name).file
46      if (file.exists())
47        props.load(new java.io.FileReader(file))
48      props
49    }
50    else
51      props
52  }
53
54  private def compute_timing(results: Build.Results, group: Option[String]): Timing =
55  {
56    val timings = results.sessions.collect {
57      case session if group.forall(results.info(session).groups.contains(_)) =>
58        results(session).timing
59    }
60    (Timing.zero /: timings)(_ + _)
61  }
62
63  private def with_documents(options: Options): Options =
64  {
65    if (documents)
66      options
67        .bool.update("browser_info", true)
68        .string.update("document", "pdf")
69        .string.update("document_variants", "document:outline=/proof,/ML")
70    else
71      options
72  }
73
74
75  final def hg_id(path: Path): String =
76    Mercurial.repository(path).id()
77
78  final def print_section(title: String): Unit =
79    println(s"\n=== $title ===\n")
80
81
82  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
83  final val isabelle_id = hg_id(isabelle_home)
84  final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
85
86
87  override final def apply(args: List[String]): Unit =
88  {
89    print_section("CONFIGURATION")
90    println(Build_Log.Settings.show())
91    val props = load_properties()
92    System.getProperties().asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props)
93
94    val options =
95      with_documents(Options.init())
96        .int.update("parallel_proofs", 1)
97        .int.update("threads", threads)
98
99    print_section("BUILD")
100    println(s"Build started at $start_time")
101    println(s"Isabelle id $isabelle_id")
102    pre_hook(args)
103
104    print_section("LOG")
105    val (results, elapsed_time) = build(options)
106
107    print_section("TIMING")
108
109    val groups = results.sessions.map(results.info).flatMap(_.groups)
110    for (group <- groups)
111      println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
112
113    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
114    println("Overall: " + total_timing.message_resources)
115
116    if (!results.ok) {
117      print_section("FAILED SESSIONS")
118
119      for (name <- results.sessions) {
120        if (results.cancelled(name)) {
121          println(s"Session $name: CANCELLED")
122        }
123        else {
124          val result = results(name)
125          if (!result.ok)
126            println(s"Session $name: FAILED ${result.rc}")
127        }
128      }
129    }
130
131    post_hook(results)
132
133    System.exit(results.rc)
134  }
135
136
137  /* profile */
138
139  def documents: Boolean = true
140  def clean: Boolean = true
141  def numa: Boolean = false
142
143  def threads: Int
144  def jobs: Int
145  def include: List[Path]
146  def select: List[Path]
147
148  def pre_hook(args: List[String]): Unit
149  def post_hook(results: Build.Results): Unit
150
151  def selection: Sessions.Selection
152}
153