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