1.1 --- a/src/Pure/ML/ml_statistics.scala Fri Jan 18 22:31:57 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,119 +0,0 @@
1.4 -/* Title: Pure/ML/ml_statistics.ML
1.5 - Author: Makarius
1.6 -
1.7 -ML runtime statistics.
1.8 -*/
1.9 -
1.10 -package isabelle
1.11 -
1.12 -
1.13 -import scala.collection.immutable.{SortedSet, SortedMap}
1.14 -import scala.swing.{Frame, Component}
1.15 -
1.16 -import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
1.17 -import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
1.18 -import org.jfree.chart.plot.PlotOrientation
1.19 -
1.20 -
1.21 -object ML_Statistics
1.22 -{
1.23 - /* content interpretation */
1.24 -
1.25 - final case class Entry(time: Double, data: Map[String, Double])
1.26 -
1.27 - def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
1.28 - def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
1.29 -
1.30 - val empty = apply(Nil)
1.31 -
1.32 -
1.33 - /* standard fields */
1.34 -
1.35 - val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
1.36 -
1.37 - val heap_fields =
1.38 - ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
1.39 - "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
1.40 -
1.41 - val threads_fields =
1.42 - ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
1.43 - "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
1.44 -
1.45 - val time_fields =
1.46 - ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
1.47 -
1.48 - val tasks_fields =
1.49 - ("Future tasks",
1.50 - List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
1.51 -
1.52 - val workers_fields =
1.53 - ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
1.54 -
1.55 - val standard_fields =
1.56 - List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
1.57 -}
1.58 -
1.59 -final class ML_Statistics private(val stats: List[Properties.T])
1.60 -{
1.61 - val Now = new Properties.Double("now")
1.62 - def now(props: Properties.T): Double = Now.unapply(props).get
1.63 -
1.64 - require(stats.forall(props => Now.unapply(props).isDefined))
1.65 -
1.66 - val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
1.67 - val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
1.68 -
1.69 - val fields: Set[String] =
1.70 - SortedSet.empty[String] ++
1.71 - (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
1.72 - yield x)
1.73 -
1.74 - val content: List[ML_Statistics.Entry] =
1.75 - stats.map(props => {
1.76 - val time = now(props) - time_start
1.77 - require(time >= 0.0)
1.78 - val data =
1.79 - SortedMap.empty[String, Double] ++
1.80 - (for ((x, y) <- props.iterator if x != Now.name)
1.81 - yield (x, java.lang.Double.parseDouble(y)))
1.82 - ML_Statistics.Entry(time, data)
1.83 - })
1.84 -
1.85 -
1.86 - /* charts */
1.87 -
1.88 - def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
1.89 - {
1.90 - data.removeAllSeries
1.91 - for {
1.92 - field <- selected_fields.iterator
1.93 - series = new XYSeries(field)
1.94 - } {
1.95 - content.foreach(entry => series.add(entry.time, entry.data(field)))
1.96 - data.addSeries(series)
1.97 - }
1.98 - }
1.99 -
1.100 - def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
1.101 - {
1.102 - val data = new XYSeriesCollection
1.103 - update_data(data, selected_fields)
1.104 -
1.105 - ChartFactory.createXYLineChart(title, "time", "value", data,
1.106 - PlotOrientation.VERTICAL, true, true, true)
1.107 - }
1.108 -
1.109 - def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
1.110 -
1.111 - def standard_frames: Unit =
1.112 - ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
1.113 - Swing_Thread.later {
1.114 - new Frame {
1.115 - iconImage = Isabelle_System.get_icon().getImage
1.116 - title = "ML statistics"
1.117 - contents = Component.wrap(new ChartPanel(c))
1.118 - visible = true
1.119 - }
1.120 - })
1.121 -}
1.122 -
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Pure/Tools/ml_statistics.scala Fri Jan 18 22:38:34 2013 +0100
2.3 @@ -0,0 +1,119 @@
2.4 +/* Title: Pure/ML/ml_statistics.ML
2.5 + Author: Makarius
2.6 +
2.7 +ML runtime statistics.
2.8 +*/
2.9 +
2.10 +package isabelle
2.11 +
2.12 +
2.13 +import scala.collection.immutable.{SortedSet, SortedMap}
2.14 +import scala.swing.{Frame, Component}
2.15 +
2.16 +import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
2.17 +import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
2.18 +import org.jfree.chart.plot.PlotOrientation
2.19 +
2.20 +
2.21 +object ML_Statistics
2.22 +{
2.23 + /* content interpretation */
2.24 +
2.25 + final case class Entry(time: Double, data: Map[String, Double])
2.26 +
2.27 + def apply(stats: List[Properties.T]): ML_Statistics = new ML_Statistics(stats)
2.28 + def apply(path: Path): ML_Statistics = apply(Build.parse_log(File.read_gzip(path)).stats)
2.29 +
2.30 + val empty = apply(Nil)
2.31 +
2.32 +
2.33 + /* standard fields */
2.34 +
2.35 + val GC_fields = ("GCs", List("partial_GCs", "full_GCs"))
2.36 +
2.37 + val heap_fields =
2.38 + ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
2.39 + "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
2.40 +
2.41 + val threads_fields =
2.42 + ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
2.43 + "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
2.44 +
2.45 + val time_fields =
2.46 + ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
2.47 +
2.48 + val tasks_fields =
2.49 + ("Future tasks",
2.50 + List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
2.51 +
2.52 + val workers_fields =
2.53 + ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
2.54 +
2.55 + val standard_fields =
2.56 + List(GC_fields, heap_fields, threads_fields, time_fields, tasks_fields, workers_fields)
2.57 +}
2.58 +
2.59 +final class ML_Statistics private(val stats: List[Properties.T])
2.60 +{
2.61 + val Now = new Properties.Double("now")
2.62 + def now(props: Properties.T): Double = Now.unapply(props).get
2.63 +
2.64 + require(stats.forall(props => Now.unapply(props).isDefined))
2.65 +
2.66 + val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
2.67 + val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
2.68 +
2.69 + val fields: Set[String] =
2.70 + SortedSet.empty[String] ++
2.71 + (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
2.72 + yield x)
2.73 +
2.74 + val content: List[ML_Statistics.Entry] =
2.75 + stats.map(props => {
2.76 + val time = now(props) - time_start
2.77 + require(time >= 0.0)
2.78 + val data =
2.79 + SortedMap.empty[String, Double] ++
2.80 + (for ((x, y) <- props.iterator if x != Now.name)
2.81 + yield (x, java.lang.Double.parseDouble(y)))
2.82 + ML_Statistics.Entry(time, data)
2.83 + })
2.84 +
2.85 +
2.86 + /* charts */
2.87 +
2.88 + def update_data(data: XYSeriesCollection, selected_fields: Iterable[String])
2.89 + {
2.90 + data.removeAllSeries
2.91 + for {
2.92 + field <- selected_fields.iterator
2.93 + series = new XYSeries(field)
2.94 + } {
2.95 + content.foreach(entry => series.add(entry.time, entry.data(field)))
2.96 + data.addSeries(series)
2.97 + }
2.98 + }
2.99 +
2.100 + def chart(title: String, selected_fields: Iterable[String]): JFreeChart =
2.101 + {
2.102 + val data = new XYSeriesCollection
2.103 + update_data(data, selected_fields)
2.104 +
2.105 + ChartFactory.createXYLineChart(title, "time", "value", data,
2.106 + PlotOrientation.VERTICAL, true, true, true)
2.107 + }
2.108 +
2.109 + def chart(arg: (String, Iterable[String])): JFreeChart = chart(arg._1, arg._2)
2.110 +
2.111 + def show_standard_frames(): Unit =
2.112 + ML_Statistics.standard_fields.map(chart(_)).foreach(c =>
2.113 + Swing_Thread.later {
2.114 + new Frame {
2.115 + iconImage = Isabelle_System.get_icon().getImage
2.116 + title = "Statistics"
2.117 + contents = Component.wrap(new ChartPanel(c))
2.118 + visible = true
2.119 + }
2.120 + })
2.121 +}
2.122 +
3.1 --- a/src/Pure/build-jars Fri Jan 18 22:31:57 2013 +0100
3.2 +++ b/src/Pure/build-jars Fri Jan 18 22:38:34 2013 +0100
3.3 @@ -30,7 +30,6 @@
3.4 Isar/outer_syntax.scala
3.5 Isar/parse.scala
3.6 Isar/token.scala
3.7 - ML/ml_statistics.scala
3.8 PIDE/command.scala
3.9 PIDE/document.scala
3.10 PIDE/markup.scala
3.11 @@ -65,6 +64,7 @@
3.12 Tools/build.scala
3.13 Tools/build_dialog.scala
3.14 Tools/main.scala
3.15 + Tools/ml_statistics.scala
3.16 Tools/task_statistics.scala
3.17 library.scala
3.18 package.scala