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