--- 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
--- 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>\<open>-v\<close> prints all messages from the session database, including
- extra information and tracing messages etc.
+ \<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database that are
+ normally inlined into the source text, including information messages etc.
\<close>
subsubsection \<open>Examples\<close>
--- 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;
--- 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 =>
--- 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;
--- /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))
+ }
+}
--- 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"
--- 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"
--- 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
--- 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";
--- 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
--- 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
--- 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)
})
}
--- 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