src/Pure/Tools/profiling_report.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 64342 53fb4a19fb98
permissions -rw-r--r--
tuned signature;
wenzelm@64342
     1
/*  Title:      Pure/Tools/profiling_report.scala
wenzelm@64311
     2
    Author:     Makarius
wenzelm@64311
     3
wenzelm@64311
     4
Report Poly/ML profiling information from log files.
wenzelm@64311
     5
*/
wenzelm@64311
     6
wenzelm@64311
     7
package isabelle
wenzelm@64311
     8
wenzelm@64311
     9
wenzelm@64311
    10
import java.util.Locale
wenzelm@64311
    11
wenzelm@64311
    12
wenzelm@64311
    13
object Profiling_Report
wenzelm@64311
    14
{
wenzelm@64311
    15
  def profiling_report(log_file: Build_Log.Log_File): List[(Long, String)] =
wenzelm@64311
    16
  {
wenzelm@64311
    17
    val Line = """^(?:### )?([ 0-9]{10}) (\S+|GARBAGE COLLECTION.*)$""".r
wenzelm@64311
    18
    val Count = """ *(\d+)""".r
wenzelm@64311
    19
    val clean = """-?\(\d+\).*$""".r
wenzelm@64311
    20
wenzelm@64311
    21
    var results = Map.empty[String, Long]
wenzelm@64311
    22
    for (Line(Count(Value.Long(count)), raw_fun) <- log_file.lines) {
wenzelm@64311
    23
      val fun = clean.replaceAllIn(raw_fun, "")
wenzelm@64311
    24
      results += (fun -> (results.getOrElse(fun, 0L) + count))
wenzelm@64311
    25
    }
wenzelm@64311
    26
    for ((fun, count) <- results.toList.sortBy(_._2)) yield (count, fun)
wenzelm@64311
    27
  }
wenzelm@64311
    28
wenzelm@64311
    29
wenzelm@64311
    30
  /* Isabelle tool wrapper */
wenzelm@64311
    31
wenzelm@64311
    32
  val isabelle_tool =
wenzelm@64311
    33
    Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args =>
wenzelm@64311
    34
    {
wenzelm@64311
    35
      Command_Line.tool0 {
wenzelm@64311
    36
        val getopts =
wenzelm@64311
    37
          Getopts("""
wenzelm@64311
    38
Usage: isabelle profiling_report [LOGS ...]
wenzelm@64311
    39
wenzelm@64311
    40
  Report Poly/ML profiling output from log files (potentially compressed).
wenzelm@64311
    41
""")
wenzelm@64311
    42
        val log_names = getopts(args)
wenzelm@64311
    43
        for (name <- log_names) {
wenzelm@64311
    44
          val log_file = Build_Log.Log_File(Path.explode(name))
wenzelm@64311
    45
          val results =
wenzelm@64311
    46
            for ((count, fun) <- profiling_report(log_file))
wenzelm@64311
    47
              yield
wenzelm@64311
    48
                String.format(Locale.ROOT, "%14d %s",
wenzelm@64311
    49
                  count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef])
wenzelm@64311
    50
          if (results.nonEmpty)
wenzelm@64311
    51
            Output.writeln(cat_lines((log_file.name + ":") :: results))
wenzelm@64311
    52
        }
wenzelm@64311
    53
      }
wenzelm@64311
    54
    })
wenzelm@64311
    55
}