diff options
author | Paul Steckler <steck@stecksoft.com> | 2017-08-15 10:31:09 -0400 |
---|---|---|
committer | Paul Steckler <steck@stecksoft.com> | 2017-08-17 11:40:26 -0400 |
commit | 51d4d83316f91abb25ea331bfdc1dcba17362dc8 (patch) | |
tree | 25eb115f4faeb87d6ae0d3db687f3111fdcf1886 /kernel | |
parent | 63da901edc3ab5b69098499cdc01ab50ed9b3353 (diff) |
Add native compute profiling, BZ#5170
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
-rw-r--r-- | kernel/nativelib.ml | 32 | ||||
-rw-r--r-- | kernel/nativelib.mli | 2 |
3 files changed, 24 insertions, 12 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d2f050d3b..a62a079da 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -132,7 +132,7 @@ let native_conv_gen pb sigma env univs t1 t2 = let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code penv sigma prefix t1 t2 in - match compile ml_filename code with + match compile ml_filename code ~profile:false with | (true, fn) -> begin if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 02e02b031..665ddf7a6 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -64,7 +64,7 @@ let warn_native_compiler_failed = in CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print -let call_compiler ml_filename = +let call_compiler ?profile:(profile=false) ml_filename = let load_path = !get_load_paths () in let load_path = List.map (fun dn -> dn / output_dir) load_path in let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in @@ -74,14 +74,26 @@ let call_compiler ml_filename = let remove f = if Sys.file_exists f then Sys.remove f in remove link_filename; remove (f ^ ".cmi"); + let initial_args = + if Dynlink.is_native then + ["opt"; "-shared"] + else + ["ocamlc"; "-c"] + in + let profile_args = + if profile then + ["-g"] + else + [] + in let args = - (if Dynlink.is_native then "opt" else "ocamlc") - ::(if Dynlink.is_native then "-shared" else "-c") - ::"-o"::link_filename - ::"-rectypes" - ::"-w"::"a" - ::include_dirs - @ ["-impl"; ml_filename] in + initial_args @ + profile_args @ + ("-o"::link_filename + ::"-rectypes" + ::"-w"::"a" + ::include_dirs) @ + ["-impl"; ml_filename] in if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (ocamlfind ()) args in @@ -95,9 +107,9 @@ let call_compiler ml_filename = warn_native_compiler_failed (Inr e); false, link_filename -let compile fn code = +let compile fn code ~profile:profile = write_ml_code fn code; - let r = call_compiler fn in + let r = call_compiler ~profile fn in if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; r diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index e8b51dc36..a262a9f58 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -19,7 +19,7 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string -val compile : string -> global list -> bool * string +val compile : string -> global list -> profile:bool -> bool * string val compile_library : Names.dir_path -> global list -> string -> bool |