<commit_before>/*  Title:      Pure/ML/task_statistics.ML
    Author:     Makarius

Future task runtime statistics.
*/

package isabelle


import scala.swing.{Frame, Component}

import org.jfree.data.statistics.HistogramDataset
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
import org.jfree.chart.plot.{XYPlot, PlotOrientation}
import org.jfree.chart.renderer.xy.{XYBarRenderer, StandardXYBarPainter}


object Task_Statistics
{
  def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
    new Task_Statistics(name, tasks)

  def apply(info: Build.Log_Info): Task_Statistics =
    apply(info.name, info.tasks)
}

final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
{
  private val Task_Name = new Properties.String("task_name")
  private val Run = new Properties.Int("run")

  def chart(bins: Int = 100): JFreeChart =
  {
    val values = new Array[Double](tasks.length)
    for ((Run(x), i) <- tasks.iterator.zipWithIndex) values(i) =
      Math.log10(x.toDouble / 1000000)

    val data = new HistogramDataset
    data.addSeries("tasks", values, bins)

    val c =
      ChartFactory.createHistogram("Task runtime distribution",
        "log10(runtime / s)", "number of tasks", data,
        PlotOrientation.VERTICAL, true, true, true)
<commit_msg>accomodate scala-2.9.2;<commit_after>/*  Title:      Pure/ML/task_statistics.ML
    Author:     Makarius

Future task runtime statistics.
*/

package isabelle


import scala.swing.{Frame, Component}

import org.jfree.data.statistics.HistogramDataset
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
import org.jfree.chart.plot.{XYPlot, PlotOrientation}
import org.jfree.chart.renderer.xy.{XYBarRenderer, StandardXYBarPainter}


object Task_Statistics
{
  def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
    new Task_Statistics(name, tasks)

  def apply(info: Build.Log_Info): Task_Statistics =
    apply(info.name, info.tasks)
}

final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
{
  private val Task_Name = new Properties.String("task_name")
  private val Run = new Properties.Int("run")

  def chart(bins: Int = 100): JFreeChart =
  {
    val values = new Array[Double](tasks.length)
    for ((Run(x), i) <- tasks.iterator.zipWithIndex) values(i) =
      java.lang.Math.log10(x.toDouble / 1000000)

    val data = new HistogramDataset
    data.addSeries("tasks", values, bins)

    val c =
      ChartFactory.createHistogram("Task runtime distribution",
        "log10(runtime / s)", "number of tasks", data,
        PlotOrientation.VERTICAL, true, true, true)

{'fraction_non_alphanumeric': 0.11715797430083144, 'fraction_numerical': 0.011715797430083144, 'mean_word_length': 4.139805825242719, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1196069', 'n_tokens_mistral': 879, 'n_tokens_neox': 833, 'n_words': 201}