# HG changeset patch # User wenzelm # Date 1358545114 -3600 # Node ID 1791a90a94fbcc7967aba53a83c198d6b5ab3b60 # Parent bc746aa3e8d5207e51c47d6dfe24b08d2e9557ea tuned signature; diff -r bc746aa3e8d5 -r 1791a90a94fb src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Fri Jan 18 22:31:57 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,119 +0,0 @@ -/* Title: Pure/ML/ml_statistics.ML - Author: Makarius - -ML runtime statistics. -*/ - -package isabelle - - -import scala.collection.immutable.{SortedSet, SortedMap} -import scala.swing.{Frame, Component} - -import org.jfree.data.xy.{XYSeries, XYSeriesCollection} -import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} -import org.jfree.chart.plot.PlotOrientation - - -object ML_Statistics -{ - /* content interpretation */ - - final case class Entry(time: Double, data: Map[String, Double]) - - def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats) - def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats) - - val empty = apply(Nil) - - - /* standard fields */ - - val GC_fields = ("GCs", List("partial_GCs", "full_GCs")) - - val heap_fields = - ("Heap", List("size_heap", "size_allocation", "size_allocation_free", - "size_heap_free_last_full_GC", "size_heap_free_last_GC")) - - val threads_fields = - ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", - "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) - - val time_fields = - ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user")) - - val tasks_fields = - ("Future tasks", - List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive")) - - val workers_fields = - ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) - - val standard_fields = - List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields) -} - -final class ML_Statistics private(val stats: List[Properties.T]) -{ - val Now = new Properties.Double("now") - def now(props: Properties.T): Double = Now.unapply(props).get - - require(stats.forall(props => Now.unapply(props).isDefined)) - - val time_start = if (stats.isEmpty) 0.0 else now(stats.head) - val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start - - val fields: Set[String] = - SortedSet.empty[String] ++ - (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name) - yield x) - - val content: List[ML_Statistics.Entry] = - stats.map(props => { - val time = now(props) - time_start - require(time >= 0.0) - val data = - SortedMap.empty[String, Double] ++ - (for ((x, y) <- props.iterator if x != Now.name) - yield (x, java.lang.Double.parseDouble(y))) - ML_Statistics.Entry(time, data) - }) - - - /* charts */ - - def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) - { - data.removeAllSeries - for { - field <- selected_fields.iterator - series = new XYSeries(field) - } { - content.foreach(entry => series.add(entry.time, entry.data(field))) - data.addSeries(series) - } - } - - def chart(title: String, selected_fields: Iterable[String]): JFreeChart = - { - val data = new XYSeriesCollection - update_data(data, selected_fields) - - ChartFactory.createXYLineChart(title, "time", "value", data, - PlotOrientation.VERTICAL, true, true, true) - } - - def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2) - - def standard_frames: Unit = - ML_Statistics.standard_fields.map(chart(_)).foreach(c => - Swing_Thread.later { - new Frame { - iconImage = Isabelle_System.get_icon().getImage - title = "ML statistics" - contents = Component.wrap(new ChartPanel(c)) - visible = true - } - }) -} - diff -r bc746aa3e8d5 -r 1791a90a94fb src/Pure/Tools/ml_statistics.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/ml_statistics.scala Fri Jan 18 22:38:34 2013 +0100 @@ -0,0 +1,119 @@ +/* Title: Pure/ML/ml_statistics.ML + Author: Makarius + +ML runtime statistics. +*/ + +package isabelle + + +import scala.collection.immutable.{SortedSet, SortedMap} +import scala.swing.{Frame, Component} + +import org.jfree.data.xy.{XYSeries, XYSeriesCollection} +import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} +import org.jfree.chart.plot.PlotOrientation + + +object ML_Statistics +{ + /* content interpretation */ + + final case class Entry(time: Double, data: Map[String, Double]) + + def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats) + def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats) + + val empty = apply(Nil) + + + /* standard fields */ + + val GC_fields = ("GCs", List("partial_GCs", "full_GCs")) + + val heap_fields = + ("Heap", List("size_heap", "size_allocation", "size_allocation_free", + "size_heap_free_last_full_GC", "size_heap_free_last_GC")) + + val threads_fields = + ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", + "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) + + val time_fields = + ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user")) + + val tasks_fields = + ("Future tasks", + List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive")) + + val workers_fields = + ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) + + val standard_fields = + List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields) +} + +final class ML_Statistics private(val stats: List[Properties.T]) +{ + val Now = new Properties.Double("now") + def now(props: Properties.T): Double = Now.unapply(props).get + + require(stats.forall(props => Now.unapply(props).isDefined)) + + val time_start = if (stats.isEmpty) 0.0 else now(stats.head) + val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start + + val fields: Set[String] = + SortedSet.empty[String] ++ + (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name) + yield x) + + val content: List[ML_Statistics.Entry] = + stats.map(props => { + val time = now(props) - time_start + require(time >= 0.0) + val data = + SortedMap.empty[String, Double] ++ + (for ((x, y) <- props.iterator if x != Now.name) + yield (x, java.lang.Double.parseDouble(y))) + ML_Statistics.Entry(time, data) + }) + + + /* charts */ + + def update_data(data: XYSeriesCollection, selected_fields: Iterable[String]) + { + data.removeAllSeries + for { + field <- selected_fields.iterator + series = new XYSeries(field) + } { + content.foreach(entry => series.add(entry.time, entry.data(field))) + data.addSeries(series) + } + } + + def chart(title: String, selected_fields: Iterable[String]): JFreeChart = + { + val data = new XYSeriesCollection + update_data(data, selected_fields) + + ChartFactory.createXYLineChart(title, "time", "value", data, + PlotOrientation.VERTICAL, true, true, true) + } + + def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2) + + def show_standard_frames(): Unit = + ML_Statistics.standard_fields.map(chart(_)).foreach(c => + Swing_Thread.later { + new Frame { + iconImage = Isabelle_System.get_icon().getImage + title = "Statistics" + contents = Component.wrap(new ChartPanel(c)) + visible = true + } + }) +} + diff -r bc746aa3e8d5 -r 1791a90a94fb src/Pure/build-jars --- a/src/Pure/build-jars Fri Jan 18 22:31:57 2013 +0100 +++ b/src/Pure/build-jars Fri Jan 18 22:38:34 2013 +0100 @@ -30,7 +30,6 @@ Isar/outer_syntax.scala Isar/parse.scala Isar/token.scala - ML/ml_statistics.scala PIDE/command.scala PIDE/document.scala PIDE/markup.scala @@ -65,6 +64,7 @@ Tools/build.scala Tools/build_dialog.scala Tools/main.scala + Tools/ml_statistics.scala Tools/task_statistics.scala library.scala package.scala