tuned signature;
authorwenzelm
Fri Jan 18 22:38:34 2013 +0100 (2013-01-18)
changeset 509811791a90a94fb
parent 50980 bc746aa3e8d5
child 50982 a7aa17a1f721
tuned signature;
src/Pure/ML/ml_statistics.scala
src/Pure/Tools/ml_statistics.scala
src/Pure/build-jars
     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