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 + "system_heaps",
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        selection = selection)
32    }
33    val end_time = Time.now()
34    (results, end_time - start_time)
35  }
36
37  private def load_properties(): JProperties =
38  {
39    val props = new JProperties()
40    val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES")
41
42    if (file_name != "")
43    {
44      val file = Path.explode(file_name).file
45      if (file.exists())
46        props.load(new java.io.FileReader(file))
47      props
48    }
49    else
50      props
51  }
52
53  private def compute_timing(results: Build.Results, group: Option[String]): Timing =
54  {
55    val timings = results.sessions.collect {
56      case session if group.forall(results.info(session).groups.contains(_)) =>
57        results(session).timing
58    }
59    (Timing.zero /: timings)(_ + _)
60  }
61
62  private def with_documents(options: Options): Options =
63  {
64    if (documents)
65      options
66        .bool.update("browser_info", true)
67        .string.update("document", "pdf")
68        .string.update("document_variants", "document:outline=/proof,/ML")
69    else
70      options
71  }
72
73
74  final def hg_id(path: Path): String =
75    Mercurial.repository(path).id()
76
77  final def print_section(title: String): Unit =
78    println(s"\n=== $title ===\n")
79
80
81  final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
82  final val isabelle_id = hg_id(isabelle_home)
83  final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
84
85
86  override final def apply(args: List[String]): Unit =
87  {
88    print_section("CONFIGURATION")
89    println(Build_Log.Settings.show())
90    val props = load_properties()
91    System.getProperties().asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props)
92
93    val options =
94      with_documents(Options.init())
95        .int.update("parallel_proofs", 1)
96        .int.update("threads", threads)
97
98    println(s"jobs = $jobs, threads = $threads, numa = $numa")
99
100    print_section("BUILD")
101    println(s"Build started at $start_time")
102    println(s"Isabelle id $isabelle_id")
103    pre_hook(args)
104
105    print_section("LOG")
106    val (results, elapsed_time) = build(options)
107
108    print_section("TIMING")
109
110    val groups = results.sessions.map(results.info).flatMap(_.groups)
111    for (group <- groups)
112      println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
113
114    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
115    println("Overall: " + total_timing.message_resources)
116
117    if (!results.ok) {
118      print_section("FAILED SESSIONS")
119
120      for (name <- results.sessions) {
121        if (results.cancelled(name)) {
122          println(s"Session $name: CANCELLED")
123        }
124        else {
125          val result = results(name)
126          if (!result.ok)
127            println(s"Session $name: FAILED ${result.rc}")
128        }
129      }
130    }
131
132    post_hook(results)
133
134    System.exit(results.rc)
135  }
136
137  /* profile */
138
139  def threads: Int = Isabelle_System.hostname() match {
140    case "hpcisabelle" => 8
141    case "lxcisa1" => 4
142    case _ => 2
143  }
144
145  def jobs: Int = Isabelle_System.hostname() match {
146    case "hpcisabelle" => 8
147    case "lxcisa1" => 10
148    case _ => 2
149  }
150
151  def numa: Boolean = Isabelle_System.hostname() == "hpcisabelle"
152
153  def documents: Boolean = true
154  def clean: Boolean = true
155
156  def include: List[Path]
157  def select: List[Path]
158
159  def pre_hook(args: List[String]): Unit
160  def post_hook(results: Build.Results): Unit
161
162  def selection: Sessions.Selection
163}
164