--- a/NEWS Tue Oct 18 17:41:56 2016 +0200
+++ b/NEWS Wed Oct 19 14:42:28 2016 +0200
@@ -1033,6 +1033,9 @@
exhaust the small 32-bit address space of the ML process (which is used
by default).
+* System option "profiling" specifies the mode for global ML profiling
+in "isabelle build". Possible values are "time", "allocations".
+
* System option "ML_process_policy" specifies an optional command prefix
for the underlying ML process, e.g. to control CPU affinity on
multiprocessor systems. The "isabelle jedit" tool allows to override the
--- a/etc/options Tue Oct 18 17:41:56 2016 +0200
+++ b/etc/options Wed Oct 19 14:42:28 2016 +0200
@@ -108,6 +108,9 @@
option checkpoint : bool = false
-- "checkpoint for theories during build process (heap compression)"
+option profiling : string = ""
+ -- "ML profiling (possible values: time, allocations)"
+
section "ML System"
--- a/src/Doc/System/Sessions.thy Tue Oct 18 17:41:56 2016 +0200
+++ b/src/Doc/System/Sessions.thy Wed Oct 19 14:42:28 2016 +0200
@@ -215,6 +215,11 @@
Isabelle/Scala. Thus it is relatively reliable in canceling processes that
get out of control, even if there is a deadlock without CPU time usage.
+ \<^item> @{system_option_def "profiling"} specifies a mode for global ML
+ profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
+ @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
+ Results appear near the bottom of the session log file.
+
The @{tool_def options} tool prints Isabelle system options. Its
command-line usage is:
@{verbatim [display]
--- a/src/Pure/Tools/build.ML Tue Oct 18 17:41:56 2016 +0200
+++ b/src/Pure/Tools/build.ML Wed Oct 19 14:42:28 2016 +0200
@@ -114,6 +114,12 @@
symbols = symbols,
last_timing = last_timing,
master_dir = master_dir}
+ |>
+ (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