tuned signature;
authorwenzelm
Tue Oct 04 19:26:19 2016 +0200 (2016-10-04)
changeset 64041fd454d9e97c4
parent 64040 84f283385091
child 64042 6957bd29a950
tuned signature;
src/Pure/Tools/build.scala
src/Pure/Tools/ci_api.scala
src/Pure/Tools/ml_statistics.scala
src/Pure/Tools/task_statistics.scala
     1.1 --- a/src/Pure/Tools/build.scala	Tue Oct 04 18:26:26 2016 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Oct 04 19:26:19 2016 +0200
     1.3 @@ -348,31 +348,30 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* log files */
     1.8 +  /* session log files */
     1.9  
    1.10    private val SESSION_NAME = "\fSession.name = "
    1.11  
    1.12 -  sealed case class Log_Info(
    1.13 -    name: String,
    1.14 -    stats: List[Properties.T],
    1.15 -    tasks: List[Properties.T],
    1.16 +  sealed case class Session_Log_Info(
    1.17 +    session_name: String,
    1.18 +    session_timing: Properties.T,
    1.19      command_timings: List[Properties.T],
    1.20 -    session_timing: Properties.T)
    1.21 +    ml_statistics: List[Properties.T],
    1.22 +    task_statistics: List[Properties.T])
    1.23  
    1.24 -  def parse_log(full_stats: Boolean, text: String): Log_Info =
    1.25 +  def parse_session_log(lines: List[String], full: Boolean): Session_Log_Info =
    1.26    {
    1.27 -    val lines = split_lines(text)
    1.28      val xml_cache = new XML.Cache()
    1.29      def parse_lines(prfx: String): List[Properties.T] =
    1.30        Props.parse_lines(prfx, lines).map(xml_cache.props(_))
    1.31  
    1.32 -    val name =
    1.33 +    val session_name =
    1.34        lines.find(_.startsWith(SESSION_NAME)).map(_.substring(SESSION_NAME.length)) getOrElse ""
    1.35 -    val stats = if (full_stats) parse_lines("\fML_statistics = ") else Nil
    1.36 -    val tasks = if (full_stats) parse_lines("\ftask_statistics = ") else Nil
    1.37 +    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    1.38      val command_timings = parse_lines("\fcommand_timing = ")
    1.39 -    val session_timing = Props.find_parse_line("\fTiming = ", lines) getOrElse Nil
    1.40 -    Log_Info(name, stats, tasks, command_timings, session_timing)
    1.41 +    val ml_statistics = if (full) parse_lines("\fML_statistics = ") else Nil
    1.42 +    val task_statistics = if (full) parse_lines("\ftask_statistics = ") else Nil
    1.43 +    Session_Log_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    1.44    }
    1.45  
    1.46  
    1.47 @@ -519,7 +518,7 @@
    1.48        }
    1.49  
    1.50        try {
    1.51 -        val info = parse_log(false, text)
    1.52 +        val info = parse_session_log(split_lines(text), false)
    1.53          val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    1.54          (info.command_timings, session_timing)
    1.55        }
     2.1 --- a/src/Pure/Tools/ci_api.scala	Tue Oct 04 18:26:26 2016 +0200
     2.2 +++ b/src/Pure/Tools/ci_api.scala	Tue Oct 04 19:26:19 2016 +0200
     2.3 @@ -45,9 +45,12 @@
     2.4      session_logs: List[(String, URL)])
     2.5    {
     2.6      def read_output(): String = Url.read(output)
     2.7 -    def read_log(full_stats: Boolean, name: String): Build.Log_Info =
     2.8 -      Build.parse_log(full_stats,
     2.9 -        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    2.10 +    def read_log(name: String, full: Boolean): Build.Session_Log_Info =
    2.11 +    {
    2.12 +      val text =
    2.13 +        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    2.14 +      Build.parse_session_log(split_lines(text), full)
    2.15 +    }
    2.16    }
    2.17  
    2.18    def build_job_builds(job_name: String): List[Build_Info] =
     3.1 --- a/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 18:26:26 2016 +0200
     3.2 +++ b/src/Pure/Tools/ml_statistics.scala	Tue Oct 04 19:26:19 2016 +0200
     3.3 @@ -22,11 +22,11 @@
     3.4  
     3.5    final case class Entry(time: Double, data: Map[String, Double])
     3.6  
     3.7 -  def apply(name: String, stats: List[Properties.T]): ML_Statistics =
     3.8 -    new ML_Statistics(name, stats)
     3.9 +  def apply(session_name: String, ml_statistics: List[Properties.T]): ML_Statistics =
    3.10 +    new ML_Statistics(session_name, ml_statistics)
    3.11  
    3.12 -  def apply(info: Build.Log_Info): ML_Statistics =
    3.13 -    apply(info.name, info.stats)
    3.14 +  def apply(info: Build.Session_Log_Info): ML_Statistics =
    3.15 +    apply(info.session_name, info.ml_statistics)
    3.16  
    3.17    val empty = apply("", Nil)
    3.18  
    3.19 @@ -59,26 +59,26 @@
    3.20        time_fields, speed_fields)
    3.21  }
    3.22  
    3.23 -final class ML_Statistics private(val name: String, val stats: List[Properties.T])
    3.24 +final class ML_Statistics private(val session_name: String, val ml_statistics: List[Properties.T])
    3.25  {
    3.26    val Now = new Properties.Double("now")
    3.27    def now(props: Properties.T): Double = Now.unapply(props).get
    3.28  
    3.29 -  require(stats.forall(props => Now.unapply(props).isDefined))
    3.30 +  require(ml_statistics.forall(props => Now.unapply(props).isDefined))
    3.31  
    3.32 -  val time_start = if (stats.isEmpty) 0.0 else now(stats.head)
    3.33 -  val duration = if (stats.isEmpty) 0.0 else now(stats.last) - time_start
    3.34 +  val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
    3.35 +  val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
    3.36  
    3.37    val fields: Set[String] =
    3.38      SortedSet.empty[String] ++
    3.39 -      (for (props <- stats.iterator; (x, _) <- props.iterator if x != Now.name)
    3.40 +      (for (props <- ml_statistics.iterator; (x, _) <- props.iterator if x != Now.name)
    3.41          yield x)
    3.42  
    3.43    val content: List[ML_Statistics.Entry] =
    3.44    {
    3.45      var last_edge = Map.empty[String, (Double, Double, Double)]
    3.46      val result = new mutable.ListBuffer[ML_Statistics.Entry]
    3.47 -    for (props <- stats) {
    3.48 +    for (props <- ml_statistics) {
    3.49        val time = now(props) - time_start
    3.50        require(time >= 0.0)
    3.51  
    3.52 @@ -135,7 +135,7 @@
    3.53        GUI_Thread.later {
    3.54          new Frame {
    3.55            iconImage = GUI.isabelle_image()
    3.56 -          title = name
    3.57 +          title = session_name
    3.58            contents = Component.wrap(new ChartPanel(c))
    3.59            visible = true
    3.60          }
     4.1 --- a/src/Pure/Tools/task_statistics.scala	Tue Oct 04 18:26:26 2016 +0200
     4.2 +++ b/src/Pure/Tools/task_statistics.scala	Tue Oct 04 19:26:19 2016 +0200
     4.3 @@ -17,22 +17,23 @@
     4.4  
     4.5  object Task_Statistics
     4.6  {
     4.7 -  def apply(name: String, tasks: List[Properties.T]): Task_Statistics =
     4.8 -    new Task_Statistics(name, tasks)
     4.9 +  def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics =
    4.10 +    new Task_Statistics(session_name, task_statistics)
    4.11  
    4.12 -  def apply(info: Build.Log_Info): Task_Statistics =
    4.13 -    apply(info.name, info.tasks)
    4.14 +  def apply(info: Build.Session_Log_Info): Task_Statistics =
    4.15 +    apply(info.session_name, info.task_statistics)
    4.16  }
    4.17  
    4.18 -final class Task_Statistics private(val name: String, val tasks: List[Properties.T])
    4.19 +final class Task_Statistics private(
    4.20 +  val session_name: String, val task_statistics: List[Properties.T])
    4.21  {
    4.22    private val Task_Name = new Properties.String("task_name")
    4.23    private val Run = new Properties.Int("run")
    4.24  
    4.25    def chart(bins: Int = 100): JFreeChart =
    4.26    {
    4.27 -    val values = new Array[Double](tasks.length)
    4.28 -    for ((Run(x), i) <- tasks.iterator.zipWithIndex)
    4.29 +    val values = new Array[Double](task_statistics.length)
    4.30 +    for ((Run(x), i) <- task_statistics.iterator.zipWithIndex)
    4.31        values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000)
    4.32  
    4.33      val data = new HistogramDataset
    4.34 @@ -54,7 +55,7 @@
    4.35      GUI_Thread.later {
    4.36        new Frame {
    4.37          iconImage = GUI.isabelle_image()
    4.38 -        title = name
    4.39 +        title = session_name
    4.40          contents = Component.wrap(new ChartPanel(chart(bins)))
    4.41          visible = true
    4.42        }