# HG changeset patch # User wenzelm # Date 1477132498 -7200 # Node ID 53fb4a19fb9847e54dec604d7e7fad945266e00a # Parent 45b6faeee56d216f1427f7a2642350af82d14fc5 regular user tool; diff -r 45b6faeee56d -r 53fb4a19fb98 NEWS --- a/NEWS Sat Oct 22 12:34:17 2016 +0200 +++ b/NEWS Sat Oct 22 12:34:58 2016 +0200 @@ -1041,7 +1041,9 @@ by default). * System option "profiling" specifies the mode for global ML profiling -in "isabelle build". Possible values are "time", "allocations". +in "isabelle build". Possible values are "time", "allocations". The +command-line tool "isabelle profiling_report" helps to digest the +resulting log files. * System option "ML_process_policy" specifies an optional command prefix for the underlying ML process, e.g. to control CPU affinity on diff -r 45b6faeee56d -r 53fb4a19fb98 src/Pure/Admin/profiling_report.scala --- a/src/Pure/Admin/profiling_report.scala Sat Oct 22 12:34:17 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,55 +0,0 @@ -/* Title: Pure/Admin/profiling_report.scala - Author: Makarius - -Report Poly/ML profiling information from log files. -*/ - -package isabelle - - -import java.util.Locale - - -object Profiling_Report -{ - def profiling_report(log_file: Build_Log.Log_File): List[(Long, String)] = - { - val Line = """^(?:### )?([ 0-9]{10}) (\S+|GARBAGE COLLECTION.*)$""".r - val Count = """ *(\d+)""".r - val clean = """-?\(\d+\).*$""".r - - var results = Map.empty[String, Long] - for (Line(Count(Value.Long(count)), raw_fun) <- log_file.lines) { - val fun = clean.replaceAllIn(raw_fun, "") - results += (fun -> (results.getOrElse(fun, 0L) + count)) - } - for ((fun, count) <- results.toList.sortBy(_._2)) yield (count, fun) - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = - Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args => - { - Command_Line.tool0 { - val getopts = - Getopts(""" -Usage: isabelle profiling_report [LOGS ...] - - Report Poly/ML profiling output from log files (potentially compressed). -""") - val log_names = getopts(args) - for (name <- log_names) { - val log_file = Build_Log.Log_File(Path.explode(name)) - val results = - for ((count, fun) <- profiling_report(log_file)) - yield - String.format(Locale.ROOT, "%14d %s", - count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef]) - if (results.nonEmpty) - Output.writeln(cat_lines((log_file.name + ":") :: results)) - } - } - }) -} diff -r 45b6faeee56d -r 53fb4a19fb98 src/Pure/Tools/profiling_report.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/profiling_report.scala Sat Oct 22 12:34:58 2016 +0200 @@ -0,0 +1,55 @@ +/* Title: Pure/Tools/profiling_report.scala + Author: Makarius + +Report Poly/ML profiling information from log files. +*/ + +package isabelle + + +import java.util.Locale + + +object Profiling_Report +{ + def profiling_report(log_file: Build_Log.Log_File): List[(Long, String)] = + { + val Line = """^(?:### )?([ 0-9]{10}) (\S+|GARBAGE COLLECTION.*)$""".r + val Count = """ *(\d+)""".r + val clean = """-?\(\d+\).*$""".r + + var results = Map.empty[String, Long] + for (Line(Count(Value.Long(count)), raw_fun) <- log_file.lines) { + val fun = clean.replaceAllIn(raw_fun, "") + results += (fun -> (results.getOrElse(fun, 0L) + count)) + } + for ((fun, count) <- results.toList.sortBy(_._2)) yield (count, fun) + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files", args => + { + Command_Line.tool0 { + val getopts = + Getopts(""" +Usage: isabelle profiling_report [LOGS ...] + + Report Poly/ML profiling output from log files (potentially compressed). +""") + val log_names = getopts(args) + for (name <- log_names) { + val log_file = Build_Log.Log_File(Path.explode(name)) + val results = + for ((count, fun) <- profiling_report(log_file)) + yield + String.format(Locale.ROOT, "%14d %s", + count.asInstanceOf[AnyRef], fun.asInstanceOf[AnyRef]) + if (results.nonEmpty) + Output.writeln(cat_lines((log_file.name + ":") :: results)) + } + } + }) +} diff -r 45b6faeee56d -r 53fb4a19fb98 src/Pure/build-jars --- a/src/Pure/build-jars Sat Oct 22 12:34:17 2016 +0200 +++ b/src/Pure/build-jars Sat Oct 22 12:34:58 2016 +0200 @@ -19,7 +19,6 @@ Admin/ci_profile.scala Admin/isabelle_cronjob.scala Admin/other_isabelle.scala - Admin/profiling_report.scala Admin/remote_dmg.scala Concurrent/consumer_thread.scala Concurrent/counter.scala @@ -130,6 +129,7 @@ Tools/ml_statistics.scala Tools/news.scala Tools/print_operation.scala + Tools/profiling_report.scala Tools/simplifier_trace.scala Tools/task_statistics.scala Tools/update_cartouches.scala