# HG changeset patch # User wenzelm # Date 1623230721 -7200 # Node ID 8a9fd2ffb81db7c042dab411014da39891df214e # Parent ae2f8144b60dc144fd38cc9773e6143dea49e9ea# Parent 014b944f4972cf8489756fc05ca225d9135ac59b merged diff -r ae2f8144b60d -r 8a9fd2ffb81d NEWS --- a/NEWS Tue Jun 08 17:01:32 2021 +0200 +++ b/NEWS Wed Jun 09 11:25:21 2021 +0200 @@ -237,6 +237,17 @@ *** System *** +* ML profiling has been updated and reactivated, after some degration in +Isabelle2021: + + - "isabelle build -o threads=1 -o profiling=..." works properly + within the PIDE session context; + + - "isabelle profiling_report" now uses the session build database + (like "isabelle log"); + + - output uses non-intrusive tracing messages, instead of warnings. + * System option "system_log" specifies an optional log file for internal messages produced by Output.system_message in Isabelle/ML; the value "true" refers to console progress of the build job. This works for diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Doc/System/Sessions.thy Wed Jun 09 11:25:21 2021 +0200 @@ -542,6 +542,7 @@ -U output Unicode symbols -m MARGIN margin for pretty printing (default: 76.0) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -v print all messages, including information etc. Print messages from the build database of the given session, without any checks against current sources: results from a failed build can be @@ -566,8 +567,8 @@ symbols. The default is for an old-fashioned ASCII terminal at 80 characters per line (76 + 4 characters to prefix warnings or errors). - \<^medskip> Option \<^verbatim>\-v\ prints all messages from the session database, including - extra information and tracing messages etc. + \<^medskip> Option \<^verbatim>\-v\ prints all messages from the session database that are + normally inlined into the source text, including information messages etc. \ subsubsection \Examples\ diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/General/output.ML --- a/src/Pure/General/output.ML Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/General/output.ML Wed Jun 09 11:25:21 2021 +0200 @@ -10,9 +10,6 @@ val tracing: string -> unit val warning: string -> unit val legacy_feature: string -> unit - val profile_time: ('a -> 'b) -> 'a -> 'b - val profile_time_thread: ('a -> 'b) -> 'a -> 'b - val profile_allocations: ('a -> 'b) -> 'a -> 'b end; signature OUTPUT = @@ -158,40 +155,6 @@ fun protocol_message props body = ! protocol_message_fn props body; fun try_protocol_message props body = protocol_message props body handle Protocol_Message _ => (); - -(* profiling *) - -local - -fun output_profile title 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; - -in - -fun profile_time f x = - ML_Profiling.profile_time (output_profile "time profile:") f x; - -fun profile_time_thread f x = - ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x; - -fun profile_allocations f x = - ML_Profiling.profile_allocations (output_profile "allocations profile:") f x; - -end; - - end; structure Output: OUTPUT = Private_Output; diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/Isar/runtime.ML Wed Jun 09 11:25:21 2021 +0200 @@ -194,7 +194,8 @@ f |> debugging1 opt_context |> debugging2 opt_context; fun controlled_execution opt_context f x = - (f |> debugging opt_context |> Future.interruptible_task) x; + (f |> debugging opt_context |> Future.interruptible_task + |> ML_Profiling.profile (Options.default_string "profiling")) x; fun toplevel_error output_exn f x = f x handle exn => diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/ML/ml_profiling.ML --- a/src/Pure/ML/ml_profiling.ML Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/ML/ml_profiling.ML Wed Jun 09 11:25:21 2021 +0200 @@ -1,26 +1,76 @@ (* Title: Pure/ML/ml_profiling.ML Author: Makarius -ML profiling. +ML profiling (via Poly/ML run-time system). *) +signature BASIC_ML_PROFILING = +sig + val profile_time: ('a -> 'b) -> 'a -> 'b + val profile_time_thread: ('a -> 'b) -> 'a -> 'b + val profile_allocations: ('a -> 'b) -> 'a -> 'b +end; + signature ML_PROFILING = sig - val profile_time: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b - val profile_time_thread: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b - val profile_allocations: ((int * string) list -> unit) -> ('a -> 'b) -> 'a -> 'b + val check_mode: string -> unit + val profile: string -> ('a -> 'b) -> 'a -> 'b + include BASIC_ML_PROFILING end; structure ML_Profiling: ML_PROFILING = struct -fun profile_time pr f x = - PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x; +(* mode *) + +val modes = + Symtab.make + [("time", PolyML.Profiling.ProfileTime), + ("time_thread", PolyML.Profiling.ProfileTimeThisThread), + ("allocations", PolyML.Profiling.ProfileAllocations)]; + +fun get_mode kind = + (case Symtab.lookup modes kind of + SOME mode => mode + | NONE => error ("Bad profiling mode: " ^ quote kind)); + +fun check_mode "" = () + | check_mode kind = ignore (get_mode kind); + + +(* profile *) -fun profile_time_thread pr f x = - PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x; +fun print_entry count name = + let + val c = string_of_int count; + val prefix = Symbol.spaces (Int.max (0, 12 - size c)); + in prefix ^ c ^ " " ^ name end; -fun profile_allocations pr f x = - PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x; +fun profile "" f x = f x + | profile kind f x = + let + val mode = get_mode kind; + fun output 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 head = XML.Text ("profile_" ^ kind ^ ":\n"); + val foot = XML.Text (print_entry total "TOTAL"); + val msg = XML.Elem (Markup.ML_profiling kind, head :: body @ [foot]); + in tracing (YXML.string_of msg) end); + in PolyML.Profiling.profileStream output mode f x end; + +fun profile_time f = profile "time" f; +fun profile_time_thread f = profile "time_thread" f; +fun profile_allocations f = profile "allocations" f; end; + +structure Basic_ML_Profiling: BASIC_ML_PROFILING = ML_Profiling; +open Basic_ML_Profiling; diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/ML/ml_profiling.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_profiling.scala Wed Jun 09 11:25:21 2021 +0200 @@ -0,0 +1,49 @@ +/* Title: Pure/ML/ml_profiling.scala + Author: Makarius + +ML profiling (via Poly/ML run-time system). +*/ + +package isabelle + + +import java.util.Locale + +import scala.collection.immutable.SortedMap + + +object ML_Profiling +{ + sealed case class Entry(name: String, count: Long) + { + def clean_name: Entry = copy(name = """-?$\d+$.*$""".r.replaceAllIn(name, "")) + + def print: String = + String.format(Locale.ROOT, "%12d %s", + count.asInstanceOf[AnyRef], name.asInstanceOf[AnyRef]) + } + + sealed case class Report(kind: String, entries: List[Entry]) + { + def clean_name: Report = copy(entries = entries.map(_.clean_name)) + + def total: Entry = Entry("TOTAL", entries.iterator.map(_.count).sum) + + def print: String = + ("profile_" + kind + ":\n") + cat_lines((entries ::: List(total)).map(_.print)) + } + + def account(reports: List[Report]): List[Report] = + { + val empty = SortedMap.empty[String, Long].withDefaultValue(0L) + var results = SortedMap.empty[String, SortedMap[String, Long]].withDefaultValue(empty) + for (report <- reports) { + val kind = report.kind + val map = report.entries.foldLeft(results(kind))( + (m, e) => m + (e.name -> (e.count + m(e.name)))) + results = results + (kind -> map) + } + for ((kind, map) <- results.toList) + yield Report(kind, for ((name, count) <- map.toList.sortBy(_._2)) yield Entry(name, count)) + } +} diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/PIDE/markup.ML Wed Jun 09 11:25:21 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 ae2f8144b60d -r 8a9fd2ffb81d src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Jun 09 11:25:21 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 ae2f8144b60d -r 8a9fd2ffb81d src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/PIDE/protocol.scala Wed Jun 09 11:25:21 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_tracing(msg) => + Markup.ML_Profiling.unapply_report(tree) + case _ => None + } + } + + /* export */ object Export diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/ROOT.ML Wed Jun 09 11:25:21 2021 +0200 @@ -27,7 +27,6 @@ ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; -ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.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 ae2f8144b60d -r 8a9fd2ffb81d src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/Tools/build.ML Wed Jun 09 11:25:21 2021 +0200 @@ -46,6 +46,7 @@ fun build_theories qualifier (options, thys) = let + val _ = ML_Profiling.check_mode (Options.string options "profiling"); val condition = space_explode "," (Options.string options "condition"); val conds = filter_out (can getenv_strict) condition; val loaded_theories = @@ -54,12 +55,6 @@ Isabelle_Process.init_options (); Future.fork I; (Thy_Info.use_theories options qualifier - |> - (case Options.string options "profiling" of - "" => I - | "time" => profile_time - | "allocations" => profile_allocations - | bad => error ("Bad profiling option: " ^ quote bad)) |> Unsynchronized.setmp print_mode (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) else diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/Tools/build_job.scala Wed Jun 09 11:25:21 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) { @@ -170,7 +170,7 @@ -U output Unicode symbols -m MARGIN margin for pretty printing (default: """ + margin + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -v print all messages, including information, tracing etc. + -v print all messages, including information etc. Print messages from the build database of the given session, without any checks against current sources: results from a failed build can be diff -r ae2f8144b60d -r 8a9fd2ffb81d src/Pure/Tools/profiling_report.scala --- a/src/Pure/Tools/profiling_report.scala Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/Tools/profiling_report.scala Wed Jun 09 11:25:21 2021 +0200 @@ -1,29 +1,48 @@ /* 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) + (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator + } yield if (clean_name) report.clean_name else report).toList + + for (report <- ML_Profiling.account(reports)) progress.echo(report.print) + } + }) } @@ -33,22 +52,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 ae2f8144b60d -r 8a9fd2ffb81d src/Pure/build-jars --- a/src/Pure/build-jars Tue Jun 08 17:01:32 2021 +0200 +++ b/src/Pure/build-jars Wed Jun 09 11:25:21 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