--- a/src/Pure/ML/ml_profiling.ML Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/ML/ml_profiling.ML Tue Jun 08 13:17:45 2021 +0200
@@ -14,30 +14,36 @@
structure ML_Profiling: ML_PROFILING =
struct
-fun profile mode title =
- mode |> PolyML.Profiling.profileStream (fn entries =>
- let
- val body = entries
- |> sort (int_ord o apply2 fst)
- |> map (fn (count, name) =>
- let
- val c = string_of_int count;
- val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
- in prefix ^ c ^ " " ^ name end);
- val total = fold (curry (op +) o fst) entries 0;
- in
- if total = 0 then ()
- else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
- end);
+fun print_entry count name =
+ let
+ val c = string_of_int count;
+ val prefix = Symbol.spaces (Int.max (0, 10 - size c));
+ in prefix ^ c ^ " " ^ name end;
+
+fun profile mode kind title f x =
+ PolyML.Profiling.profileStream (fn entries =>
+ (case fold (curry (op +) o fst) entries 0 of
+ 0 => ()
+ | total =>
+ let
+ val body = entries
+ |> sort (int_ord o apply2 fst)
+ |> map (fn (count, name) =>
+ let val markup = Markup.ML_profiling_entry {name = name, count = count}
+ in XML.Elem (markup, [XML.Text (print_entry count name ^ "\n")]) end);
+ val xml =
+ XML.Elem (Markup.ML_profiling kind,
+ XML.Text (title ^ "\n") :: body @ [XML.Text (print_entry total "TOTAL")]);
+ in warning (YXML.string_of xml) end)) mode f x;
fun profile_time f =
- profile PolyML.Profiling.ProfileTime "time profile:" f;
+ profile PolyML.Profiling.ProfileTime "time" "time profile:" f;
fun profile_time_thread f =
- profile PolyML.Profiling.ProfileTimeThisThread "time profile (this thread):" f;
+ profile PolyML.Profiling.ProfileTimeThisThread "time_thread" "time profile (single thread):" f;
fun profile_allocations f =
- profile PolyML.Profiling.ProfileAllocations "allocations profile:" f;
+ profile PolyML.Profiling.ProfileAllocations "allocations" "allocations profile:" f;
end;
--- a/src/Pure/PIDE/markup.ML Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/PIDE/markup.ML Tue Jun 08 13:17:45 2021 +0200
@@ -202,6 +202,11 @@
val no_reportN: string val no_report: T
val badN: string val bad: unit -> T
val intensifyN: string val intensify: T
+ val countN: string
+ val ML_profiling_entryN: string
+ val ML_profiling_entry: {name: string, count: int} -> T
+ val ML_profilingN: string
+ val ML_profiling: string -> T
val browserN: string
val graphviewN: string
val theory_exportsN: string
@@ -657,6 +662,17 @@
val (intensifyN, intensify) = markup_elem "intensify";
+(* ML profiling *)
+
+val countN = "count";
+
+val ML_profiling_entryN = "ML_profiling_entry";
+fun ML_profiling_entry {name, count} =
+ (ML_profiling_entryN, [(nameN, name), (countN, Value.print_int count)]);
+
+val (ML_profilingN, ML_profiling) = markup_string "ML_profiling" kindN;
+
+
(* active areas *)
val browserN = "browser"
--- a/src/Pure/PIDE/markup.scala Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Jun 08 13:17:45 2021 +0200
@@ -564,6 +564,30 @@
val INTENSIFY = "intensify"
+ /* ML profiling */
+
+ val COUNT = "count"
+ val ML_PROFILING_ENTRY = "ML_profiling_entry"
+ val ML_PROFILING = "ML_profiling"
+
+ object ML_Profiling
+ {
+ def unapply_entry(tree: XML.Tree): Option[isabelle.ML_Profiling.Entry] =
+ tree match {
+ case XML.Elem(Markup(ML_PROFILING_ENTRY, List((NAME, name), (COUNT, Value.Long(count)))), _) =>
+ Some(isabelle.ML_Profiling.Entry(name, count))
+ case _ => None
+ }
+
+ def unapply_report(tree: XML.Tree): Option[isabelle.ML_Profiling.Report] =
+ tree match {
+ case XML.Elem(Markup(ML_PROFILING, List((KIND, kind))), body) =>
+ Some(isabelle.ML_Profiling.Report(kind, body.flatMap(unapply_entry)))
+ case _ => None
+ }
+ }
+
+
/* active areas */
val BROWSER = "browser"
--- a/src/Pure/PIDE/protocol.scala Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Jun 08 13:17:45 2021 +0200
@@ -210,6 +210,19 @@
}
+ /* ML profiling */
+
+ object ML_Profiling
+ {
+ def unapply(msg: XML.Tree): Option[isabelle.ML_Profiling.Report] =
+ msg match {
+ case XML.Elem(_, List(tree)) if is_warning(msg) =>
+ Markup.ML_Profiling.unapply_report(tree)
+ case _ => None
+ }
+ }
+
+
/* export */
object Export
--- a/src/Pure/ROOT.ML Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/ROOT.ML Tue Jun 08 13:17:45 2021 +0200
@@ -46,7 +46,6 @@
ML_file "General/properties.ML";
ML_file "General/output.ML";
ML_file "PIDE/markup.ML";
-ML_file "ML/ml_profiling.ML";
ML_file "General/utf8.ML";
ML_file "General/scan.ML";
ML_file "General/source.ML";
@@ -89,6 +88,7 @@
ML_file "General/sha1.ML";
ML_file "PIDE/yxml.ML";
+ML_file "ML/ml_profiling.ML";
ML_file "PIDE/byte_message.ML";
ML_file "PIDE/protocol_message.ML";
ML_file "PIDE/document_id.ML";
--- a/src/Pure/Tools/build_job.scala Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/Tools/build_job.scala Tue Jun 08 13:17:45 2021 +0200
@@ -93,7 +93,6 @@
unicode_symbols: Boolean = false): Unit =
{
val store = Sessions.store(options)
-
val resources = Resources.empty
val session = new Session(options, resources)
@@ -109,9 +108,10 @@
result match {
case None => error("Missing build database for session " + quote(session_name))
case Some((used_theories, errors, rc)) =>
- val bad_theories = theories.filterNot(used_theories.toSet)
- if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories))
-
+ theories.filterNot(used_theories.toSet) match {
+ case Nil =>
+ case bad => error("Unknown theories " + commas_quote(bad))
+ }
val print_theories =
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
for (thy <- print_theories) {
--- a/src/Pure/Tools/profiling_report.scala Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/Tools/profiling_report.scala Tue Jun 08 13:17:45 2021 +0200
@@ -1,29 +1,50 @@
/* Title: Pure/Tools/profiling_report.scala
Author: Makarius
-Report Poly/ML profiling information from log files.
+Report Poly/ML profiling information from session build database.
*/
package isabelle
-import java.util.Locale
-
-
object Profiling_Report
{
- def profiling_report(log_file: Build_Log.Log_File): List[(Long, String)] =
+ def profiling_report(
+ options: Options,
+ session_name: String,
+ theories: List[String] = Nil,
+ clean_name: Boolean = false,
+ progress: Progress = new Progress): Unit =
{
- val Line = """^(?:### )?([ 0-9]{10}) (\S+|GARBAGE COLLECTION.*)$""".r
- val Count = """ *(\d+)""".r
- val clean = """-?\(\d+\).*$""".r
+ val store = Sessions.store(options)
+ val resources = Resources.empty
+ val session = new Session(options, resources)
- 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)
+ using(store.open_database_context())(db_context =>
+ {
+ val result =
+ db_context.input_database(session_name)((db, name) => Some(store.read_theories(db, name)))
+ result match {
+ case None => error("Missing build database for session " + quote(session_name))
+ case Some(used_theories) =>
+ theories.filterNot(used_theories.toSet) match {
+ case Nil =>
+ case bad => error("Unknown theories " + commas_quote(bad))
+ }
+ val reports =
+ (for {
+ thy <- used_theories.iterator
+ if theories.isEmpty || theories.contains(thy)
+ command <- Build_Job.read_theory(db_context, resources, session_name, thy).iterator
+ snapshot = Document.State.init.snippet(command)
+ rendering = new Rendering(snapshot, options, session)
+ Text.Info(_, Protocol.ML_Profiling(report)) <-
+ rendering.text_messages(Text.Range.full).iterator
+ } yield if (clean_name) report.clean_name else report).toList
+
+ for (report <- ML_Profiling.account(reports)) progress.echo(report.print)
+ }
+ })
}
@@ -33,22 +54,36 @@
Isabelle_Tool("profiling_report", "report Poly/ML profiling information from log files",
Scala_Project.here, args =>
{
+ var theories: List[String] = Nil
+ var clean_name = false
+ var options = Options.init()
+
val getopts =
Getopts("""
-Usage: isabelle profiling_report [LOGS ...]
+Usage: isabelle profiling_report [OPTIONS] SESSION
+
+ Options are:
+ -T NAME restrict to given theories (multiple options possible)
+ -c clean function names
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- 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))
- }
+ Report Poly/ML profiling from the build database of the given session
+ (without up-to-date check of sources).
+""",
+ "T:" -> (arg => theories = theories ::: List(arg)),
+ "c" -> (_ => clean_name = true),
+ "o:" -> (arg => options = options + arg))
+
+ val more_args = getopts(args)
+ val session_name =
+ more_args match {
+ case List(session_name) => session_name
+ case _ => getopts.usage()
+ }
+
+ val progress = new Console_Progress()
+
+ profiling_report(options, session_name, theories = theories,
+ clean_name = clean_name, progress = progress)
})
}
--- a/src/Pure/build-jars Mon Jun 07 16:40:26 2021 +0200
+++ b/src/Pure/build-jars Tue Jun 08 13:17:45 2021 +0200
@@ -104,6 +104,7 @@
src/Pure/ML/ml_console.scala
src/Pure/ML/ml_lex.scala
src/Pure/ML/ml_process.scala
+ src/Pure/ML/ml_profiling.scala
src/Pure/ML/ml_statistics.scala
src/Pure/ML/ml_syntax.scala
src/Pure/PIDE/byte_message.scala