1/* Title: Pure/Admin/build_status.scala 2 Author: Makarius 3 4Present recent build status information from database. 5*/ 6 7package isabelle 8 9 10object Build_Status 11{ 12 /* defaults */ 13 14 val default_target_dir = Path.explode("build_status") 15 val default_image_size = (800, 600) 16 val default_history = 30 17 18 def default_profiles: List[Profile] = 19 Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles 20 21 22 /* data profiles */ 23 24 sealed case class Profile( 25 description: String, history: Int = 0, afp: Boolean = false, slow: Boolean = false, sql: String) 26 { 27 def days(options: Options): Int = options.int("build_log_history") max history 28 29 def stretch(options: Options): Double = 30 (days(options) max default_history min (default_history * 5)).toDouble / default_history 31 32 def select(options: Options, columns: List[SQL.Column], only_sessions: Set[String]): SQL.Source = 33 { 34 Build_Log.Data.universal_table.select(columns, distinct = true, 35 sql = "WHERE " + 36 Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) + 37 " AND " + 38 SQL.member(Build_Log.Data.status.ident, 39 List( 40 Build_Log.Session_Status.finished.toString, 41 Build_Log.Session_Status.failed.toString)) + 42 (if (only_sessions.isEmpty) "" 43 else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) + 44 " AND " + SQL.enclose(sql)) 45 } 46 } 47 48 49 /* build status */ 50 51 def build_status(options: Options, 52 progress: Progress = No_Progress, 53 profiles: List[Profile] = default_profiles, 54 only_sessions: Set[String] = Set.empty, 55 verbose: Boolean = false, 56 target_dir: Path = default_target_dir, 57 ml_statistics: Boolean = false, 58 image_size: (Int, Int) = default_image_size) 59 { 60 val ml_statistics_domain = 61 Iterator(ML_Statistics.heap_fields, ML_Statistics.tasks_fields, ML_Statistics.workers_fields). 62 flatMap(_._2).toSet 63 64 val data = 65 read_data(options, progress = progress, profiles = profiles, 66 only_sessions = only_sessions, verbose = verbose, 67 ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain) 68 69 present_data(data, progress = progress, target_dir = target_dir, image_size = image_size) 70 } 71 72 73 /* read data */ 74 75 sealed case class Data(date: Date, entries: List[Data_Entry]) 76 sealed case class Data_Entry( 77 name: String, hosts: List[String], stretch: Double, sessions: List[Session]) 78 { 79 def failed_sessions: List[Session] = 80 sessions.filter(_.head.failed).sortBy(_.name) 81 } 82 sealed case class Session( 83 name: String, threads: Int, entries: List[Entry], 84 ml_statistics: ML_Statistics, ml_statistics_date: Long) 85 { 86 require(entries.nonEmpty) 87 88 lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date) 89 90 def head: Entry = sorted_entries.head 91 def order: Long = - head.timing.elapsed.ms 92 93 def finished_entries: List[Entry] = sorted_entries.filter(_.finished) 94 def finished_entries_size: Int = finished_entries.map(_.date).toSet.size 95 96 def check_timing: Boolean = finished_entries_size >= 3 97 def check_heap: Boolean = 98 finished_entries_size >= 3 && 99 finished_entries.forall(entry => 100 entry.maximum_heap > 0 || 101 entry.average_heap > 0 || 102 entry.stored_heap > 0) 103 104 def make_csv: CSV.File = 105 { 106 val header = 107 List("session_name", 108 "chapter", 109 "pull_date", 110 "afp_pull_date", 111 "isabelle_version", 112 "afp_version", 113 "timing_elapsed", 114 "timing_cpu", 115 "timing_gc", 116 "ml_timing_elapsed", 117 "ml_timing_cpu", 118 "ml_timing_gc", 119 "maximum_heap", 120 "average_heap", 121 "stored_heap", 122 "status") 123 val date_format = Date.Format("uuuu-MM-dd HH:mm:ss") 124 val records = 125 for (entry <- sorted_entries) yield { 126 CSV.Record(name, 127 entry.chapter, 128 date_format(entry.pull_date), 129 entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" }, 130 entry.isabelle_version, 131 entry.afp_version, 132 entry.timing.elapsed.ms, 133 entry.timing.cpu.ms, 134 entry.timing.gc.ms, 135 entry.ml_timing.elapsed.ms, 136 entry.ml_timing.cpu.ms, 137 entry.ml_timing.gc.ms, 138 entry.maximum_heap, 139 entry.average_heap, 140 entry.stored_heap, 141 entry.status) 142 } 143 CSV.File(name, header, records) 144 } 145 } 146 sealed case class Entry( 147 chapter: String, 148 pull_date: Date, 149 afp_pull_date: Option[Date], 150 isabelle_version: String, 151 afp_version: String, 152 timing: Timing, 153 ml_timing: Timing, 154 maximum_heap: Long, 155 average_heap: Long, 156 stored_heap: Long, 157 status: Build_Log.Session_Status.Value, 158 errors: List[String]) 159 { 160 val date: Long = (afp_pull_date getOrElse pull_date).unix_epoch 161 162 def finished: Boolean = status == Build_Log.Session_Status.finished 163 def failed: Boolean = status == Build_Log.Session_Status.failed 164 165 def present_errors(name: String): XML.Body = 166 { 167 if (errors.isEmpty) 168 HTML.text(name + print_version(isabelle_version, afp_version, chapter)) 169 else { 170 HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) :: 171 HTML.text(print_version(isabelle_version, afp_version, chapter)) 172 } 173 } 174 } 175 176 sealed case class Image(name: String, width: Int, height: Int) 177 { 178 def path: Path = Path.basic(name) 179 } 180 181 def print_version( 182 isabelle_version: String, afp_version: String = "", chapter: String = "AFP"): String = 183 { 184 val body = 185 proper_string(isabelle_version).map("Isabelle/" + _).toList ::: 186 (if (chapter == "AFP") proper_string(afp_version).map("AFP/" + _) else None).toList 187 if (body.isEmpty) "" else body.mkString(" (", ", ", ")") 188 } 189 190 def read_data(options: Options, 191 progress: Progress = No_Progress, 192 profiles: List[Profile] = default_profiles, 193 only_sessions: Set[String] = Set.empty, 194 ml_statistics: Boolean = false, 195 ml_statistics_domain: String => Boolean = (key: String) => true, 196 verbose: Boolean = false): Data = 197 { 198 val date = Date.now() 199 var data_hosts = Map.empty[String, Set[String]] 200 var data_stretch = Map.empty[String, Double] 201 var data_entries = Map.empty[String, Map[String, Session]] 202 203 def get_hosts(data_name: String): Set[String] = 204 data_hosts.getOrElse(data_name, Set.empty) 205 206 val store = Build_Log.store(options) 207 208 using(store.open_database())(db => 209 { 210 for (profile <- profiles.sortBy(_.description)) { 211 progress.echo("input " + quote(profile.description)) 212 213 val afp = profile.afp 214 val columns = 215 List( 216 Build_Log.Data.pull_date(afp = false), 217 Build_Log.Data.pull_date(afp = true), 218 Build_Log.Prop.build_host, 219 Build_Log.Prop.isabelle_version, 220 Build_Log.Prop.afp_version, 221 Build_Log.Settings.ISABELLE_BUILD_OPTIONS, 222 Build_Log.Settings.ML_PLATFORM, 223 Build_Log.Data.session_name, 224 Build_Log.Data.chapter, 225 Build_Log.Data.groups, 226 Build_Log.Data.threads, 227 Build_Log.Data.timing_elapsed, 228 Build_Log.Data.timing_cpu, 229 Build_Log.Data.timing_gc, 230 Build_Log.Data.ml_timing_elapsed, 231 Build_Log.Data.ml_timing_cpu, 232 Build_Log.Data.ml_timing_gc, 233 Build_Log.Data.heap_size, 234 Build_Log.Data.status, 235 Build_Log.Data.errors) ::: 236 (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil) 237 238 val Threads_Option = """threads\s*=\s*(\d+)""".r 239 240 val sql = profile.select(options, columns, only_sessions) 241 if (verbose) progress.echo(sql) 242 243 db.using_statement(sql)(stmt => 244 { 245 val res = stmt.execute_query() 246 while (res.next()) { 247 val session_name = res.string(Build_Log.Data.session_name) 248 val chapter = res.string(Build_Log.Data.chapter) 249 val groups = split_lines(res.string(Build_Log.Data.groups)) 250 val threads = 251 { 252 val threads1 = 253 res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match { 254 case Threads_Option(Value.Int(i)) => i 255 case _ => 1 256 } 257 val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1) 258 threads1 max threads2 259 } 260 val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) 261 val data_name = 262 profile.description + 263 (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") + 264 (if (threads == 1) "" else ", " + threads + " threads") 265 266 res.get_string(Build_Log.Prop.build_host).foreach(host => 267 data_hosts += (data_name -> (get_hosts(data_name) + host))) 268 269 data_stretch += (data_name -> profile.stretch(options)) 270 271 val isabelle_version = res.string(Build_Log.Prop.isabelle_version) 272 val afp_version = res.string(Build_Log.Prop.afp_version) 273 274 val ml_stats = 275 ML_Statistics( 276 if (ml_statistics) { 277 Properties.uncompress( 278 res.bytes(Build_Log.Data.ml_statistics), cache = store.xz_cache) 279 } 280 else Nil, 281 domain = ml_statistics_domain, 282 heading = session_name + print_version(isabelle_version, afp_version, chapter)) 283 284 val entry = 285 Entry( 286 chapter = chapter, 287 pull_date = res.date(Build_Log.Data.pull_date(afp = false)), 288 afp_pull_date = 289 if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None, 290 isabelle_version = isabelle_version, 291 afp_version = afp_version, 292 timing = 293 res.timing( 294 Build_Log.Data.timing_elapsed, 295 Build_Log.Data.timing_cpu, 296 Build_Log.Data.timing_gc), 297 ml_timing = 298 res.timing( 299 Build_Log.Data.ml_timing_elapsed, 300 Build_Log.Data.ml_timing_cpu, 301 Build_Log.Data.ml_timing_gc), 302 maximum_heap = ml_stats.maximum_heap_size, 303 average_heap = ml_stats.average_heap_size, 304 stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)), 305 status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)), 306 errors = 307 Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors), 308 cache = store.xz_cache)) 309 310 val sessions = data_entries.getOrElse(data_name, Map.empty) 311 val session = 312 sessions.get(session_name) match { 313 case None => 314 Session(session_name, threads, List(entry), ml_stats, entry.date) 315 case Some(old) => 316 val (ml_stats1, ml_stats1_date) = 317 if (entry.date > old.ml_statistics_date) (ml_stats, entry.date) 318 else (old.ml_statistics, old.ml_statistics_date) 319 Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date) 320 } 321 322 if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) { 323 data_entries += (data_name -> (sessions + (session_name -> session))) 324 } 325 } 326 }) 327 } 328 }) 329 330 val sorted_entries = 331 (for { 332 (name, sessions) <- data_entries.toList 333 sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order)) 334 } 335 yield { 336 val hosts = get_hosts(name).toList.sorted 337 val stretch = data_stretch(name) 338 Data_Entry(name, hosts, stretch, sorted_sessions) 339 }).sortBy(_.name) 340 341 Data(date, sorted_entries) 342 } 343 344 345 /* present data */ 346 347 def present_data(data: Data, 348 progress: Progress = No_Progress, 349 target_dir: Path = default_target_dir, 350 image_size: (Int, Int) = default_image_size) 351 { 352 def clean_name(name: String): String = 353 name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) 354 355 def print_heap(x: Long): Option[String] = 356 if (x == 0L) None else Some(x.toString + " M") 357 358 HTML.write_document(target_dir, "index.html", 359 List(HTML.title("Isabelle build status")), 360 List(HTML.chapter("Isabelle build status"), 361 HTML.par( 362 List(HTML.description( 363 List(HTML.text("status date:") -> HTML.text(data.date.toString))))), 364 HTML.par( 365 List(HTML.itemize(data.entries.map({ case data_entry => 366 List( 367 HTML.link(clean_name(data_entry.name) + "/index.html", 368 HTML.text(data_entry.name))) ::: 369 (data_entry.failed_sessions match { 370 case Nil => Nil 371 case sessions => 372 HTML.break ::: 373 List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) ::: 374 List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name)))) 375 }) 376 })))))) 377 378 for (data_entry <- data.entries) { 379 val data_name = data_entry.name 380 381 val (image_width, image_height) = image_size 382 val image_width_stretch = (image_width * data_entry.stretch).toInt 383 384 progress.echo("output " + quote(data_name)) 385 386 val dir = target_dir + Path.basic(clean_name(data_name)) 387 Isabelle_System.mkdirs(dir) 388 389 val data_files = 390 (for (session <- data_entry.sessions) yield { 391 val csv_file = session.make_csv 392 csv_file.write(dir) 393 session.name -> csv_file 394 }).toMap 395 396 val session_plots = 397 Par_List.map((session: Session) => 398 Isabelle_System.with_tmp_file(session.name, "data") { data_file => 399 Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file => 400 401 def plot_name(kind: String): String = session.name + "_" + kind + ".png" 402 403 File.write(data_file, 404 cat_lines( 405 session.finished_entries.map(entry => 406 List(entry.date, 407 entry.timing.elapsed.minutes, 408 entry.timing.resources.minutes, 409 entry.ml_timing.elapsed.minutes, 410 entry.ml_timing.resources.minutes, 411 entry.maximum_heap, 412 entry.average_heap, 413 entry.stored_heap).mkString(" ")))) 414 415 val max_time = 416 ((0.0 /: session.finished_entries){ case (m, entry) => 417 m.max(entry.timing.elapsed.minutes). 418 max(entry.timing.resources.minutes). 419 max(entry.ml_timing.elapsed.minutes). 420 max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1 421 val timing_range = "[0:" + max_time + "]" 422 423 def gnuplot(plot_name: String, plots: List[String], range: String): Image = 424 { 425 val image = Image(plot_name, image_width_stretch, image_height) 426 427 File.write(gnuplot_file, """ 428set terminal png size """ + image.width + "," + image.height + """ 429set output """ + quote(File.standard_path(dir + image.path)) + """ 430set xdata time 431set timefmt "%s" 432set format x "%d-%b" 433set xlabel """ + quote(session.name) + """ noenhanced 434set key left bottom 435plot [] """ + range + " " + 436 plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n") 437 438 val result = 439 Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file)) 440 if (!result.ok) 441 result.error("Gnuplot failed for " + data_name + "/" + plot_name).check 442 443 image 444 } 445 446 val timing_plots = 447 { 448 val plots1 = 449 List( 450 """ using 1:2 smooth sbezier title "elapsed time (smooth)" """, 451 """ using 1:2 smooth csplines title "elapsed time" """) 452 val plots2 = 453 List( 454 """ using 1:3 smooth sbezier title "cpu time (smooth)" """, 455 """ using 1:3 smooth csplines title "cpu time" """) 456 if (session.threads == 1) plots1 else plots1 ::: plots2 457 } 458 459 val ml_timing_plots = 460 List( 461 """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """, 462 """ using 1:4 smooth csplines title "ML elapsed time" """, 463 """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """, 464 """ using 1:5 smooth csplines title "ML cpu time" """) 465 466 val heap_plots = 467 List( 468 """ using 1:6 smooth sbezier title "maximum heap (smooth)" """, 469 """ using 1:6 smooth csplines title "maximum heap" """, 470 """ using 1:7 smooth sbezier title "average heap (smooth)" """, 471 """ using 1:7 smooth csplines title "average heap" """, 472 """ using 1:8 smooth sbezier title "stored heap (smooth)" """, 473 """ using 1:8 smooth csplines title "stored heap" """) 474 475 def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image = 476 { 477 val image = Image(plot_name, image_width, image_height) 478 val chart = 479 session.ml_statistics.chart( 480 fields._1 + ": " + session.ml_statistics.heading, fields._2) 481 Graphics_File.write_chart_png( 482 (dir + image.path).file, chart, image.width, image.height) 483 image 484 } 485 486 val images = 487 (if (session.check_timing) 488 List( 489 gnuplot(plot_name("timing"), timing_plots, timing_range), 490 gnuplot(plot_name("ml_timing"), ml_timing_plots, timing_range)) 491 else Nil) ::: 492 (if (session.check_heap) 493 List(gnuplot(plot_name("heap"), heap_plots, "[0:]")) 494 else Nil) ::: 495 (if (session.ml_statistics.content.nonEmpty) 496 List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields)) ::: 497 (if (session.threads > 1) 498 List( 499 jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields), 500 jfreechart(plot_name("workers_chart"), ML_Statistics.workers_fields)) 501 else Nil) 502 else Nil) 503 504 session.name -> images 505 } 506 }, data_entry.sessions).toMap 507 508 HTML.write_document(dir, "index.html", 509 List(HTML.title("Isabelle build status for " + data_name)), 510 HTML.chapter("Isabelle build status for " + data_name) :: 511 HTML.par( 512 List(HTML.description( 513 List( 514 HTML.text("status date:") -> HTML.text(data.date.toString), 515 HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) :: 516 HTML.par( 517 List(HTML.itemize( 518 data_entry.sessions.map(session => 519 HTML.link("#session_" + session.name, HTML.text(session.name)) :: 520 HTML.text(" (" + session.head.timing.message_resources + ")"))))) :: 521 data_entry.sessions.flatMap(session => 522 List( 523 HTML.section(HTML.id("session_" + session.name), session.name), 524 HTML.par( 525 HTML.description( 526 List( 527 HTML.text("data:") -> 528 List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))), 529 HTML.text("timing:") -> HTML.text(session.head.timing.message_resources), 530 HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) ::: 531 print_heap(session.head.maximum_heap).map(s => 532 HTML.text("maximum heap:") -> HTML.text(s)).toList ::: 533 print_heap(session.head.average_heap).map(s => 534 HTML.text("average heap:") -> HTML.text(s)).toList ::: 535 print_heap(session.head.stored_heap).map(s => 536 HTML.text("stored heap:") -> HTML.text(s)).toList ::: 537 proper_string(session.head.isabelle_version).map(s => 538 HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: 539 proper_string(session.head.afp_version).map(s => 540 HTML.text("AFP version:") -> HTML.text(s)).toList) :: 541 session_plots.getOrElse(session.name, Nil).map(image => 542 HTML.size(image.width / 2, image.height / 2)(HTML.image(image.name))))))) 543 } 544 } 545 546 547 /* Isabelle tool wrapper */ 548 549 val isabelle_tool = 550 Isabelle_Tool("build_status", "present recent build status information from database", args => 551 { 552 var target_dir = default_target_dir 553 var ml_statistics = false 554 var only_sessions = Set.empty[String] 555 var options = Options.init() 556 var image_size = default_image_size 557 var verbose = false 558 559 val getopts = Getopts(""" 560Usage: isabelle build_status [OPTIONS] 561 562 Options are: 563 -D DIR target directory (default """ + default_target_dir + """) 564 -M include full ML statistics 565 -S SESSIONS only given SESSIONS (comma separated) 566 -l DAYS length of relevant history (default """ + options.int("build_log_history") + """) 567 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) 568 -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """) 569 -v verbose 570 571 Present performance statistics from build log database, which is specified 572 via system options build_log_database_host, build_log_database_user, 573 build_log_history etc. 574""", 575 "D:" -> (arg => target_dir = Path.explode(arg)), 576 "M" -> (_ => ml_statistics = true), 577 "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), 578 "l:" -> (arg => options = options + ("build_log_history=" + arg)), 579 "o:" -> (arg => options = options + arg), 580 "s:" -> (arg => 581 space_explode('x', arg).map(Value.Int.parse(_)) match { 582 case List(w, h) if w > 0 && h > 0 => image_size = (w, h) 583 case _ => error("Error bad PNG image size: " + quote(arg)) 584 }), 585 "v" -> (_ => verbose = true)) 586 587 val more_args = getopts(args) 588 if (more_args.nonEmpty) getopts.usage() 589 590 val progress = new Console_Progress 591 592 build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose, 593 target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size) 594 595 }, admin = true) 596} 597