added system option "profiling";
authorwenzelm
Wed Oct 19 14:42:28 2016 +0200 (2016-10-19)
changeset 64308b00508facb4f
parent 64307 c4d16f35c6e7
child 64309 1bde86d10013
added system option "profiling";
NEWS
etc/options
src/Doc/System/Sessions.thy
src/Pure/Tools/build.ML
     1.1 --- a/NEWS	Tue Oct 18 17:41:56 2016 +0200
     1.2 +++ b/NEWS	Wed Oct 19 14:42:28 2016 +0200
     1.3 @@ -1033,6 +1033,9 @@
     1.4  exhaust the small 32-bit address space of the ML process (which is used
     1.5  by default).
     1.6  
     1.7 +* System option "profiling" specifies the mode for global ML profiling
     1.8 +in "isabelle build". Possible values are "time", "allocations".
     1.9 +
    1.10  * System option "ML_process_policy" specifies an optional command prefix
    1.11  for the underlying ML process, e.g. to control CPU affinity on
    1.12  multiprocessor systems. The "isabelle jedit" tool allows to override the
     2.1 --- a/etc/options	Tue Oct 18 17:41:56 2016 +0200
     2.2 +++ b/etc/options	Wed Oct 19 14:42:28 2016 +0200
     2.3 @@ -108,6 +108,9 @@
     2.4  option checkpoint : bool = false
     2.5    -- "checkpoint for theories during build process (heap compression)"
     2.6  
     2.7 +option profiling : string = ""
     2.8 +  -- "ML profiling (possible values: time, allocations)"
     2.9 +
    2.10  
    2.11  section "ML System"
    2.12  
     3.1 --- a/src/Doc/System/Sessions.thy	Tue Oct 18 17:41:56 2016 +0200
     3.2 +++ b/src/Doc/System/Sessions.thy	Wed Oct 19 14:42:28 2016 +0200
     3.3 @@ -215,6 +215,11 @@
     3.4      Isabelle/Scala. Thus it is relatively reliable in canceling processes that
     3.5      get out of control, even if there is a deadlock without CPU time usage.
     3.6  
     3.7 +    \<^item> @{system_option_def "profiling"} specifies a mode for global ML
     3.8 +    profiling. Possible values are the empty string (disabled), \<^verbatim>\<open>time\<close> for
     3.9 +    @{ML profile_time} and \<^verbatim>\<open>allocations\<close> for @{ML profile_allocations}.
    3.10 +    Results appear near the bottom of the session log file.
    3.11 +
    3.12    The @{tool_def options} tool prints Isabelle system options. Its
    3.13    command-line usage is:
    3.14    @{verbatim [display]
     4.1 --- a/src/Pure/Tools/build.ML	Tue Oct 18 17:41:56 2016 +0200
     4.2 +++ b/src/Pure/Tools/build.ML	Wed Oct 19 14:42:28 2016 +0200
     4.3 @@ -114,6 +114,12 @@
     4.4            symbols = symbols,
     4.5            last_timing = last_timing,
     4.6            master_dir = master_dir}
     4.7 +        |>
     4.8 +          (case Options.string options "profiling" of
     4.9 +            "" => I
    4.10 +          | "time" => profile_time
    4.11 +          | "allocations" => profile_allocations
    4.12 +          | bad => error ("Bad profiling option: " ^ quote bad))
    4.13          |> Unsynchronized.setmp print_mode
    4.14              (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
    4.15      else