# HG changeset patch # User wenzelm # Date 1623151065 -7200 # Node ID 5dae03d50db12289cbb470ec89b1b8b49dddfb5a # Parent 364bac6691dee476ca3515a3c686711865290168 more formal ML profiling messages; diff -r 364bac6691de -r 5dae03d50db1 src/Pure/ML/ml_profiling.ML --- 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; diff -r 364bac6691de -r 5dae03d50db1 src/Pure/PIDE/markup.ML --- 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" diff -r 364bac6691de -r 5dae03d50db1 src/Pure/PIDE/markup.scala --- 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" diff -r 364bac6691de -r 5dae03d50db1 src/Pure/PIDE/protocol.scala --- 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 diff -r 364bac6691de -r 5dae03d50db1 src/Pure/ROOT.ML --- 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"; diff -r 364bac6691de -r 5dae03d50db1 src/Pure/Tools/build_job.scala --- 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) { diff -r 364bac6691de -r 5dae03d50db1 src/Pure/Tools/profiling_report.scala --- 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) }) } diff -r 364bac6691de -r 5dae03d50db1 src/Pure/build-jars --- 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