# HG changeset patch # User wenzelm # Date 1476880948 -7200 # Node ID b00508facb4fb5620d29021f3a324c47a5983222 # Parent c4d16f35c6e72c12cddfc80a0a87137faf9df497 added system option "profiling"; diff -r c4d16f35c6e7 -r b00508facb4f NEWS --- 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 diff -r c4d16f35c6e7 -r b00508facb4f etc/options --- 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" diff -r c4d16f35c6e7 -r b00508facb4f src/Doc/System/Sessions.thy --- 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>\time\ for + @{ML profile_time} and \<^verbatim>\allocations\ 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] diff -r c4d16f35c6e7 -r b00508facb4f src/Pure/Tools/build.ML --- 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