# HG changeset patch # User wenzelm # Date 1495109660 -7200 # Node ID 177b90f33f4051d54983ba739810b901a543fe70 # Parent 1945fa8f0c392f901a79cd32b8d7e97ec5fe3a86 more plots from ml_statistics; diff -r 1945fa8f0c39 -r 177b90f33f40 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Thu May 18 13:51:25 2017 +0200 +++ b/src/Pure/Admin/build_status.scala Thu May 18 14:14:20 2017 +0200 @@ -66,7 +66,8 @@ sealed case class Data(date: Date, entries: List[Data_Entry]) sealed case class Data_Entry( name: String, hosts: List[String], stretch: Double, sessions: List[Session]) - sealed case class Session(name: String, threads: Int, entries: List[Entry]) + sealed case class Session( + name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics) { require(entries.nonEmpty) @@ -91,6 +92,11 @@ average_heap: Long, final_heap: Long) + sealed case class Image(name: String, width: Int, height: Int) + { + def path: Path = Path.basic(name) + } + def read_data(options: Options, progress: Progress = No_Progress, profiles: List[Profile] = default_profiles, @@ -191,7 +197,7 @@ val sessions = data_entries.getOrElse(data_name, Map.empty) val entries = sessions.get(session_name).map(_.entries) getOrElse Nil - val session = Session(session_name, threads, entry :: entries) + val session = Session(session_name, threads, entry :: entries, ml_stats) data_entries += (data_name -> (sessions + (session_name -> session))) } }) @@ -245,8 +251,8 @@ for (data_entry <- data.entries) { val data_name = data_entry.name - val image_width = (image_size._1 * data_entry.stretch).toInt - val image_height = image_size._2 + val (image_width, image_height) = image_size + val image_width_stretch = (image_width * data_entry.stretch).toInt progress.echo("output " + quote(data_name)) @@ -258,6 +264,8 @@ Isabelle_System.with_tmp_file(session.name, "data") { data_file => Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file => + def plot_name(kind: String): String = session.name + "_" + kind + ".png" + File.write(data_file, cat_lines( session.entries.map(entry => @@ -278,13 +286,13 @@ max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1 val timing_range = "[0:" + max_time + "]" - def gnuplot(plots: List[String], kind: String, range: String): String = + def gnuplot(plot_name: String, plots: List[String], range: String): Image = { - val plot_name = session.name + "_" + kind + ".png" + val image = Image(plot_name, image_width_stretch, image_height) File.write(gnuplot_file, """ -set terminal png size """ + image_width + "," + image_height + """ -set output """ + quote(File.standard_path(dir + Path.basic(plot_name))) + """ +set terminal png size """ + image.width + "," + image.height + """ +set output """ + quote(File.standard_path(dir + image.path)) + """ set xdata time set timefmt "%s" set format x "%d-%b" @@ -298,7 +306,7 @@ if (!result.ok) result.error("Gnuplot failed for " + data_name + "/" + plot_name).check - plot_name + image } val timing_plots = @@ -330,15 +338,34 @@ """ using 1:8 smooth sbezier title "final heap (smooth)" """, """ using 1:8 smooth csplines title "final heap" """) - val plot_names = + def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image = + { + val image = Image(plot_name, image_width, image_height) + val chart = + session.ml_statistics.chart( + fields._1 + ": " + session.ml_statistics.heading, fields._2) + Graphics_File.write_chart_png( + (dir + image.path).file, chart, image.width, image.height) + image + } + + val images = (if (session.check_timing) List( - gnuplot(timing_plots, "timing", timing_range), - gnuplot(ml_timing_plots, "ml_timing", timing_range)) + gnuplot(plot_name("timing"), timing_plots, timing_range), + gnuplot(plot_name("ml_timing"), ml_timing_plots, timing_range)) + else Nil) ::: + (if (session.check_heap) + List(gnuplot(plot_name("heap"), heap_plots, "[0:]")) else Nil) ::: - (if (session.check_heap) List(gnuplot(heap_plots, "heap", "[0:]")) else Nil) + (if (session.ml_statistics.content.nonEmpty) + List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields)) ::: + (if (session.threads > 1) + List(jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields)) + else Nil) + else Nil) - session.name -> plot_names + session.name -> images } }, data_entry.sessions).toMap @@ -373,10 +400,10 @@ HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: proper_string(session.head.afp_version).map(s => HTML.text("AFP version:") -> HTML.text(s)).toList) :: - session_plots.getOrElse(session.name, Nil).map(plot_name => - HTML.image(plot_name) + - HTML.width(image_width / 2) + - HTML.height(image_height / 2)))))) + session_plots.getOrElse(session.name, Nil).map(image => + HTML.image(image.name) + + HTML.width(image.width / 2) + + HTML.height(image.height / 2)))))) } }