wenzelm@65743: /* Title: Pure/Admin/build_status.scala wenzelm@63686: Author: Makarius wenzelm@63686: wenzelm@65743: Present recent build status information from database. wenzelm@63686: */ wenzelm@63686: wenzelm@63686: package isabelle wenzelm@63686: wenzelm@63686: wenzelm@65743: object Build_Status wenzelm@63686: { wenzelm@65743: private val default_target_dir = Path.explode("build_status") wenzelm@65736: private val default_history_length = 30 wenzelm@65736: private val default_image_size = (800, 600) wenzelm@65736: wenzelm@65736: wenzelm@65736: /* data profiles */ wenzelm@63688: wenzelm@65736: sealed case class Profile(name: String, sql: String) wenzelm@65736: { wenzelm@65736: def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source = wenzelm@65736: { wenzelm@65736: val sql_sessions = wenzelm@65736: if (only_sessions.isEmpty) "" wenzelm@65736: else wenzelm@65736: only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a)) wenzelm@65736: .mkString("(", " OR ", ") AND ") wenzelm@63700: wenzelm@65736: Build_Log.Data.universal_table.select(columns, distinct = true, wenzelm@65736: sql = "WHERE " + wenzelm@65736: Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " + wenzelm@65736: Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) + wenzelm@65736: " AND " + sql_sessions + SQL.enclose(sql) + wenzelm@65736: " ORDER BY " + Build_Log.Data.pull_date + " DESC") wenzelm@65736: } wenzelm@65736: } wenzelm@65736: wenzelm@65736: val standard_profiles: List[Profile] = wenzelm@65747: Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles wenzelm@65736: wenzelm@65736: sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing) wenzelm@63688: { wenzelm@65736: def check(elapsed_threshold: Time): Boolean = wenzelm@65736: !timing.is_zero && timing.elapsed >= elapsed_threshold wenzelm@65736: } wenzelm@65736: wenzelm@65736: type Data = Map[String, Map[String, List[Entry]]] wenzelm@65736: wenzelm@63688: wenzelm@65736: /* read data */ wenzelm@65736: wenzelm@65736: def read_data(options: Options, wenzelm@65736: profiles: List[Profile] = standard_profiles, wenzelm@65736: progress: Progress = No_Progress, wenzelm@65736: history_length: Int = default_history_length, wenzelm@65736: only_sessions: Set[String] = Set.empty, wenzelm@65736: elapsed_threshold: Time = Time.zero): Data = wenzelm@65736: { wenzelm@65736: var data: Data = Map.empty wenzelm@63688: wenzelm@65736: val store = Build_Log.store(options) wenzelm@65736: using(store.open_database())(db => wenzelm@64089: { wenzelm@65736: for (profile <- profiles) { wenzelm@65742: progress.echo("input " + quote(profile.name)) wenzelm@65736: val columns = wenzelm@65736: List( wenzelm@65736: Build_Log.Data.pull_date, wenzelm@65736: Build_Log.Settings.ML_PLATFORM, wenzelm@65736: Build_Log.Data.session_name, wenzelm@65736: Build_Log.Data.threads, wenzelm@65736: Build_Log.Data.timing_elapsed, wenzelm@65736: Build_Log.Data.timing_cpu, wenzelm@65736: Build_Log.Data.timing_gc, wenzelm@65736: Build_Log.Data.ml_timing_elapsed, wenzelm@65736: Build_Log.Data.ml_timing_cpu, wenzelm@65736: Build_Log.Data.ml_timing_gc) wenzelm@63700: wenzelm@65736: db.using_statement(profile.select(columns, history_length, only_sessions))(stmt => wenzelm@65736: { wenzelm@65740: val res = stmt.execute_query() wenzelm@65740: while (res.next()) { wenzelm@65740: val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM) wenzelm@65740: val threads = res.get_int(Build_Log.Data.threads) wenzelm@65736: val name = wenzelm@65736: profile.name + wenzelm@65736: "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") + wenzelm@65736: "_M" + threads.getOrElse(1) wenzelm@63703: wenzelm@65740: val session = res.string(Build_Log.Data.session_name) wenzelm@65736: val entry = wenzelm@65740: Entry(res.date(Build_Log.Data.pull_date), wenzelm@65741: res.timing( wenzelm@65741: Build_Log.Data.timing_elapsed, wenzelm@65741: Build_Log.Data.timing_cpu, wenzelm@65741: Build_Log.Data.timing_gc), wenzelm@65741: res.timing( wenzelm@65741: Build_Log.Data.ml_timing_elapsed, wenzelm@65741: Build_Log.Data.ml_timing_cpu, wenzelm@65741: Build_Log.Data.ml_timing_gc)) wenzelm@65736: wenzelm@65736: val session_entries = data.getOrElse(name, Map.empty) wenzelm@65736: val entries = session_entries.getOrElse(session, Nil) wenzelm@65736: data += (name -> (session_entries + (session -> (entry :: entries)))) wenzelm@65736: } wenzelm@65736: }) wenzelm@65736: } wenzelm@65736: }) wenzelm@65736: wenzelm@65736: for { wenzelm@65736: (name, session_entries) <- data wenzelm@65736: session_entries1 <- wenzelm@65736: { wenzelm@65736: val session_entries1 = wenzelm@65736: for { wenzelm@65736: (session, entries) <- session_entries wenzelm@65736: if entries.filter(_.check(elapsed_threshold)).length >= 3 wenzelm@65736: } yield (session, entries) wenzelm@65736: if (session_entries1.isEmpty) None wenzelm@65736: else Some(session_entries1) wenzelm@65736: } wenzelm@65736: } yield (name, session_entries1) wenzelm@65736: } wenzelm@65736: wenzelm@65736: wenzelm@65736: /* present data */ wenzelm@65736: wenzelm@65736: private val html_header = """ wenzelm@65736: wenzelm@65743: Build status wenzelm@65736: wenzelm@65736: """ wenzelm@65736: private val html_footer = """ wenzelm@65736: wenzelm@65736: wenzelm@65736: """ wenzelm@63688: wenzelm@65736: def present_data(data: Data, wenzelm@65736: progress: Progress = No_Progress, wenzelm@65736: target_dir: Path = default_target_dir, wenzelm@65736: image_size: (Int, Int) = default_image_size, wenzelm@65736: ml_timing: Option[Boolean] = None) wenzelm@65736: { wenzelm@65736: val data_entries = data.toList.sortBy(_._1) wenzelm@65736: for ((name, session_entries) <- data_entries) { wenzelm@65736: val dir = target_dir + Path.explode(name) wenzelm@65742: progress.echo("output " + dir) wenzelm@65736: Isabelle_System.mkdirs(dir) wenzelm@65736: wenzelm@65736: for ((session, entries) <- session_entries) { wenzelm@65736: Isabelle_System.with_tmp_file(session, "data") { data_file => wenzelm@65736: Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file => wenzelm@63706: wenzelm@65736: File.write(data_file, wenzelm@65736: cat_lines( wenzelm@65736: entries.map(entry => wenzelm@65736: List(entry.date.unix_epoch.toString, wenzelm@65736: entry.timing.elapsed.minutes, wenzelm@65736: entry.timing.cpu.minutes, wenzelm@65736: entry.ml_timing.elapsed.minutes, wenzelm@65736: entry.ml_timing.cpu.minutes, wenzelm@65736: entry.ml_timing.gc.minutes).mkString(" ")))) wenzelm@65736: wenzelm@65736: val plots1 = wenzelm@65736: List( wenzelm@65736: """ using 1:3 smooth sbezier title "cpu time (smooth)" """, wenzelm@65736: """ using 1:3 smooth csplines title "cpu time" """, wenzelm@65736: """ using 1:2 smooth sbezier title "elapsed time (smooth)" """, wenzelm@65736: """ using 1:2 smooth csplines title "elapsed time" """) wenzelm@65736: val plots2 = wenzelm@65736: List( wenzelm@65736: """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """, wenzelm@65736: """ using 1:5 smooth csplines title "ML cpu time" """, wenzelm@65736: """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """, wenzelm@65736: """ using 1:4 smooth csplines title "ML elapsed time" """, wenzelm@65736: """ using 1:6 smooth sbezier title "ML gc time (smooth)" """, wenzelm@65736: """ using 1:6 smooth csplines title "ML gc time" """) wenzelm@65736: val plots = wenzelm@65736: ml_timing match { wenzelm@65736: case None => plots1 wenzelm@65736: case Some(false) => plots1 ::: plots2 wenzelm@65736: case Some(true) => plots2 wenzelm@65736: } wenzelm@65736: wenzelm@65736: File.write(gnuplot_file, """ wenzelm@65736: set terminal png size """ + image_size._1 + "," + image_size._2 + """ wenzelm@63688: set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """ wenzelm@63688: set xdata time wenzelm@63688: set timefmt "%s" wenzelm@63688: set format x "%d-%b" wenzelm@63701: set xlabel """ + quote(session) + """ noenhanced wenzelm@63688: set key left top wenzelm@64220: plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n") wenzelm@65736: wenzelm@65736: val result = wenzelm@65736: Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file)) wenzelm@65736: if (result.rc != 0) wenzelm@65742: result.error("Gnuplot failed for " + name + "/" + session).check wenzelm@63688: } wenzelm@63688: } wenzelm@63688: } wenzelm@65736: wenzelm@65736: File.write(dir + Path.basic("index.html"), wenzelm@65736: html_header + "\n

" + HTML.output(name) + "

\n" + wenzelm@65736: cat_lines( wenzelm@65736: session_entries.toList.map(_._1).sorted.map(session => wenzelm@65736: """

""")) + wenzelm@65736: "\n" + html_footer) wenzelm@63688: } wenzelm@63703: wenzelm@65736: File.write(target_dir + Path.basic("index.html"), wenzelm@65736: html_header + "\n\n" + html_footer) wenzelm@63688: } wenzelm@63688: wenzelm@63688: wenzelm@63688: /* Isabelle tool wrapper */ wenzelm@63688: wenzelm@63688: val isabelle_tool = wenzelm@65743: Isabelle_Tool("build_status", "present recent build status information from database", args => wenzelm@63688: { wenzelm@65736: var target_dir = default_target_dir wenzelm@65736: var ml_timing: Option[Boolean] = None wenzelm@65736: var only_sessions = Set.empty[String] wenzelm@65736: var elapsed_threshold = Time.zero wenzelm@63700: var history_length = default_history_length wenzelm@65736: var options = Options.init() wenzelm@65736: var image_size = default_image_size wenzelm@63688: wenzelm@63688: val getopts = Getopts(""" wenzelm@65743: Usage: isabelle build_status [OPTIONS] wenzelm@63688: wenzelm@63688: Options are: wenzelm@65737: -D DIR target directory (default """ + default_target_dir + """) wenzelm@63706: -M only ML timing wenzelm@63700: -S SESSIONS only given SESSIONS (comma separated) wenzelm@63700: -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes) wenzelm@65737: -l LENGTH length of history (default """ + default_history_length + """) wenzelm@63706: -m include ML timing wenzelm@65736: -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) wenzelm@65737: -s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """) wenzelm@63688: wenzelm@65736: Present performance statistics from build log database, which is specified wenzelm@65736: via system options build_log_database_host, build_log_database_user etc. wenzelm@63688: """, wenzelm@63688: "D:" -> (arg => target_dir = Path.explode(arg)), wenzelm@63706: "M" -> (_ => ml_timing = Some(true)), wenzelm@63700: "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), wenzelm@63805: "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))), wenzelm@63805: "l:" -> (arg => history_length = Value.Int.parse(arg)), wenzelm@63706: "m" -> (_ => ml_timing = Some(false)), wenzelm@65736: "o:" -> (arg => options = options + arg), wenzelm@63700: "s:" -> (arg => wenzelm@63805: space_explode('x', arg).map(Value.Int.parse(_)) match { wenzelm@65736: case List(w, h) if w > 0 && h > 0 => image_size = (w, h) wenzelm@63700: case _ => error("Error bad PNG image size: " + quote(arg)) wenzelm@63700: })) wenzelm@63688: wenzelm@65736: val more_args = getopts(args) wenzelm@65736: if (more_args.nonEmpty) getopts.usage() wenzelm@63700: wenzelm@65736: val progress = new Console_Progress wenzelm@63688: wenzelm@65736: val data = wenzelm@65745: read_data(options, progress = progress, history_length = history_length, wenzelm@65745: only_sessions = only_sessions, elapsed_threshold = elapsed_threshold) wenzelm@63703: wenzelm@65736: present_data(data, progress = progress, target_dir = target_dir, wenzelm@65736: image_size = image_size, ml_timing = ml_timing) wenzelm@65736: wenzelm@64161: }, admin = true) wenzelm@63686: }