diff options
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 59 |
1 files changed, 42 insertions, 17 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 02e02b031a..f784509b6f 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Nativevalues @@ -64,7 +66,8 @@ 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 () = assert Coq_config.native_compiler in 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 +77,37 @@ 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 flambda_args = + if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then + (* We play safe for now, and use the native compiler + with -Oclassic, however it is likely that `native_compute` + users can benefit from tweaking here. + *) + ["-Oclassic"] + 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 @ + flambda_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 +121,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 @@ -134,9 +160,8 @@ let call_linker ?(fatal=true) prefix f upds = register_native_file prefix with Dynlink.Error e as exn -> let exn = CErrors.push exn in - let msg = "Dynlink error, " ^ Dynlink.error_message e in - if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) - else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); + if fatal then iraise exn + else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = |