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