wenzelm@64161: /* Title: Pure/Admin/build_stats.scala wenzelm@63686: Author: Makarius wenzelm@63686: wenzelm@63686: Statistics from session build output. wenzelm@63686: */ wenzelm@63686: wenzelm@63686: package isabelle wenzelm@63686: wenzelm@63686: wenzelm@63686: object Build_Stats wenzelm@63686: { wenzelm@63688: /* presentation */ wenzelm@63688: wenzelm@63700: private val default_history_length = 100 wenzelm@63700: private val default_size = (800, 600) wenzelm@63700: private val default_only_sessions = Set.empty[String] wenzelm@63700: private val default_elapsed_threshold = Time.zero wenzelm@63706: private val default_ml_timing: Option[Boolean] = None wenzelm@63700: wenzelm@63703: def present_job(job: String, dir: Path, wenzelm@63700: history_length: Int = default_history_length, wenzelm@63700: size: (Int, Int) = default_size, wenzelm@63700: only_sessions: Set[String] = default_only_sessions, wenzelm@63706: elapsed_threshold: Time = default_elapsed_threshold, wenzelm@63706: ml_timing: Option[Boolean] = default_ml_timing): List[String] = wenzelm@63688: { wenzelm@64054: val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length) wenzelm@64054: if (job_infos.isEmpty) error("No build infos for job " + quote(job)) wenzelm@63688: wenzelm@64054: val all_infos = wenzelm@64054: Par_List.map((job_info: CI_API.Job_Info) => wenzelm@64106: (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos) wenzelm@63688: val all_sessions = wenzelm@64054: (Set.empty[String] /: all_infos)( wenzelm@64085: { case (s, (_, info)) => s ++ info.sessions.keySet }) wenzelm@63688: wenzelm@64085: def check_threshold(info: Build_Log.Build_Info, session: String): Boolean = wenzelm@64089: { wenzelm@64089: val t = info.timing(session) wenzelm@64089: !t.is_zero && t.elapsed >= elapsed_threshold wenzelm@64089: } wenzelm@63700: wenzelm@63703: val sessions = wenzelm@63703: for { wenzelm@63703: session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions) wenzelm@64054: if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3 wenzelm@63703: } yield session wenzelm@63703: wenzelm@63703: Isabelle_System.mkdirs(dir) wenzelm@63703: for (session <- sessions) { wenzelm@63688: Isabelle_System.with_tmp_file(session, "png") { data_file => wenzelm@63688: Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file => wenzelm@63688: val data = wenzelm@64085: for { (t, info) <- all_infos if info.finished(session) } wenzelm@63688: yield { wenzelm@64085: val timing1 = info.timing(session) wenzelm@64085: val timing2 = info.ml_timing(session) wenzelm@64085: List(t.toString, wenzelm@64085: timing1.elapsed.minutes, wenzelm@64085: timing1.cpu.minutes, wenzelm@64085: timing2.elapsed.minutes, wenzelm@64085: timing2.cpu.minutes, wenzelm@64085: timing2.gc.minutes).mkString(" ") wenzelm@63688: } wenzelm@63688: File.write(data_file, cat_lines(data)) wenzelm@63688: wenzelm@63706: val plots1 = wenzelm@63706: List( wenzelm@63707: """ using 1:3 smooth sbezier title "cpu time (smooth)" """, wenzelm@63707: """ using 1:3 smooth csplines title "cpu time" """, wenzelm@63706: """ using 1:2 smooth sbezier title "elapsed time (smooth)" """, wenzelm@63707: """ using 1:2 smooth csplines title "elapsed time" """) wenzelm@63706: val plots2 = wenzelm@63706: List( wenzelm@63707: """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """, wenzelm@63707: """ using 1:5 smooth csplines title "ML cpu time" """, wenzelm@63706: """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """, wenzelm@63706: """ using 1:4 smooth csplines title "ML elapsed time" """, wenzelm@63706: """ using 1:6 smooth sbezier title "ML gc time (smooth)" """, wenzelm@63706: """ using 1:6 smooth csplines title "ML gc time" """) wenzelm@63706: val plots = wenzelm@63706: ml_timing match { wenzelm@63706: case None => plots1 wenzelm@63706: case Some(false) => plots1 ::: plots2 wenzelm@63706: case Some(true) => plots2 wenzelm@63706: } wenzelm@63706: wenzelm@63706: val data_file_name = File.standard_path(data_file.getAbsolutePath) wenzelm@63688: File.write(plot_file, """ wenzelm@63700: set terminal png size """ + size._1 + "," + 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@63706: plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n") wenzelm@63688: val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file)) wenzelm@63688: if (result.rc != 0) { wenzelm@63688: Output.error_message("Session " + session + ": gnuplot error") wenzelm@63688: result.print wenzelm@63688: } wenzelm@63688: } wenzelm@63688: } wenzelm@63688: } wenzelm@63703: wenzelm@63703: sessions.toList.sorted wenzelm@63688: } wenzelm@63688: wenzelm@63688: wenzelm@63688: /* Isabelle tool wrapper */ wenzelm@63688: wenzelm@63703: private val html_header = """ wenzelm@63703: wenzelm@63703: Performance statistics from session build output wenzelm@63703: wenzelm@63703: """ wenzelm@63703: private val html_footer = """ wenzelm@63703: wenzelm@63703: wenzelm@63703: """ wenzelm@63703: wenzelm@63688: val isabelle_tool = wenzelm@63688: Isabelle_Tool("build_stats", "present statistics from session build output", args => wenzelm@63688: { wenzelm@63703: var target_dir = Path.explode("stats") wenzelm@63706: var ml_timing = default_ml_timing wenzelm@63700: var only_sessions = default_only_sessions wenzelm@63700: var elapsed_threshold = default_elapsed_threshold wenzelm@63700: var history_length = default_history_length wenzelm@63700: var size = default_size wenzelm@63688: wenzelm@63688: val getopts = Getopts(""" wenzelm@63700: Usage: isabelle build_stats [OPTIONS] [JOBS ...] wenzelm@63688: wenzelm@63688: Options are: wenzelm@63688: -D DIR target directory (default "stats") 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@63688: -l LENGTH length of history (default 100) wenzelm@63706: -m include ML timing wenzelm@63700: -s WxH size of PNG image (default 800x600) wenzelm@63688: wenzelm@63700: Present statistics from session build output of the given JOBS, from Jenkins wenzelm@63700: continuous build service specified as URL via ISABELLE_JENKINS_ROOT. 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@63700: "s:" -> (arg => wenzelm@63805: space_explode('x', arg).map(Value.Int.parse(_)) match { wenzelm@63700: case List(w, h) if w > 0 && h > 0 => size = (w, h) wenzelm@63700: case _ => error("Error bad PNG image size: " + quote(arg)) wenzelm@63700: })) wenzelm@63688: wenzelm@63700: val jobs = getopts(args) wenzelm@63688: val all_jobs = CI_API.build_jobs() wenzelm@63700: val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted wenzelm@63700: wenzelm@63700: if (jobs.isEmpty) wenzelm@63984: error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" ")) wenzelm@63700: wenzelm@63700: if (bad_jobs.nonEmpty) wenzelm@63984: error("Unknown build jobs: " + bad_jobs.mkString(" ") + wenzelm@63984: "\nAvailable jobs: " + all_jobs.sorted.mkString(" ")) wenzelm@63688: wenzelm@63688: for (job <- jobs) { wenzelm@63703: val dir = target_dir + Path.basic(job) wenzelm@63703: Output.writeln(dir.implode) wenzelm@63706: val sessions = wenzelm@63706: present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing) wenzelm@63703: File.write(dir + Path.basic("index.html"), wenzelm@63703: html_header + "\n

" + HTML.output(job) + "

\n" + wenzelm@63703: cat_lines( wenzelm@63703: sessions.map(session => wenzelm@63703: """

""")) + wenzelm@63703: "\n" + html_footer) wenzelm@63688: } wenzelm@63703: wenzelm@63703: File.write(target_dir + Path.basic("index.html"), wenzelm@63703: html_header + "\n\n" + html_footer) wenzelm@64161: }, admin = true) wenzelm@63686: }