diff options
| author |  Paul Steckler <steck@stecksoft.com> | 2017-08-17 11:25:26 -0400 |
|---|---|---|
| committer | Paul Steckler <steck@stecksoft.com> | 2017-08-18 17:08:02 -0400 |
| commit | 3f4963f4523bbc4a079a7669de3a3fb3126f3a2a (patch) | |
| tree | 4ac0896249d08b59e3685aa0d95cdd0ca4731f46 /pretyping/nativenorm.ml | |
| parent | 51d4d83316f91abb25ea331bfdc1dcba17362dc8 (diff) | |
move filename search to start_profiler
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index de0afd5e3..5b191b1e2 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -436,11 +436,10 @@ let evars_of_evar_map sigma = Nativelambda.evars_metas = Evd.meta_type sigma } (* fork perf process, return profiler's process id *) -let start_profiler_linux () = +let start_profiler_linux profile_fn = let coq_pid = Unix.getpid () in (* pass pid of running coqtop *) (* we don't want to see perf's console output *) let dev_null = Unix.descr_of_out_channel (open_out_bin "/dev/null") in - let profile_fn = get_available_profile_filename () in let _ = Feedback.msg_info (Pp.str ("Profiling to file " ^ profile_fn)) in let perf = "perf" in let profiler_pid = @@ -468,8 +467,9 @@ let stop_profiler_linux m_pid = | None -> () let start_profiler () = + let profile_fn = get_available_profile_filename () in match profiler_platform () with - "Unix (Linux)" -> start_profiler_linux () + "Unix (Linux)" -> start_profiler_linux profile_fn | _ -> let _ = Feedback.msg_info (Pp.str (Format.sprintf "Native_compute profiling not supported on the platform: %s" |