# HG changeset patch # User wenzelm # Date 1471210516 -7200 # Node ID ec095a532a2bb5b7960a6322007da4aa0cde9155 # Parent fed1d4dab990ee9d6671137141d9fc122cfc9d06 provide index.html; tuned; diff -r fed1d4dab990 -r ec095a532a2b src/Pure/Tools/build_stats.scala --- a/src/Pure/Tools/build_stats.scala Sun Aug 14 22:48:23 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Sun Aug 14 23:35:16 2016 +0200 @@ -75,25 +75,20 @@ /* presentation */ - private val default_target_dir = Path.explode("stats") private val default_history_length = 100 private val default_size = (800, 600) private val default_only_sessions = Set.empty[String] private val default_elapsed_threshold = Time.zero - def present(job: String, - target_dir: Path = default_target_dir, + def present_job(job: String, dir: Path, history_length: Int = default_history_length, size: (Int, Int) = default_size, only_sessions: Set[String] = default_only_sessions, - elapsed_threshold: Time = default_elapsed_threshold) + elapsed_threshold: Time = default_elapsed_threshold): List[String] = { val build_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length) if (build_infos.isEmpty) error("No build infos for job " + quote(job)) - val dir = target_dir + Path.basic(job) - Isabelle_System.mkdirs(dir) - val all_build_stats = Par_List.map((info: CI_API.Build_Info) => (info.timestamp / 1000, parse(Url.read(info.output))), build_infos) @@ -107,10 +102,14 @@ case None => false } - for { - session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions) - if all_build_stats.filter({ case (_, stats) => check_threshold(stats, session) }).length >= 3 - } { + val sessions = + for { + session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions) + if all_build_stats.filter({ case (_, stats) => check_threshold(stats, session) }).length >= 3 + } yield session + + Isabelle_System.mkdirs(dir) + for (session <- sessions) { Isabelle_System.with_tmp_file(session, "png") { data_file => Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file => val data = @@ -144,15 +143,27 @@ } } } + + sessions.toList.sorted } /* Isabelle tool wrapper */ + private val html_header = """ + +Performance statistics from session build output + +""" + private val html_footer = """ + + +""" + val isabelle_tool = Isabelle_Tool("build_stats", "present statistics from session build output", args => { - var target_dir = default_target_dir + var target_dir = Path.explode("stats") var only_sessions = default_only_sessions var elapsed_threshold = default_elapsed_threshold var history_length = default_history_length @@ -193,10 +204,24 @@ "\nAvailable jobs: " + commas(all_jobs.sorted)) for (job <- jobs) { - Output.writeln((target_dir + Path.basic(job)).implode) - present(job, target_dir, history_length, size, only_sessions, elapsed_threshold) + val dir = target_dir + Path.basic(job) + Output.writeln(dir.implode) + val sessions = present_job(job, dir, history_length, size, only_sessions, elapsed_threshold) + File.write(dir + Path.basic("index.html"), + html_header + "\n

" + HTML.output(job) + "

\n" + + cat_lines( + sessions.map(session => + """

""")) + + "\n" + html_footer) } - }) + + File.write(target_dir + Path.basic("index.html"), + html_header + "\n\n" + html_footer) + }) } sealed case class Build_Stats(