diff options
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 65 |
1 files changed, 45 insertions, 20 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1c58c744..f784509b 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-2016 *) +(* * 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 @@ -15,7 +17,7 @@ open Envars used by the native compiler. *) let get_load_paths = - ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized") : unit -> string list) + ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized.") : unit -> string list) let open_header = ["Nativevalues"; "Nativecode"; @@ -35,7 +37,7 @@ let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed until flags have been properly initialized *) let include_dirs () = - [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"] + [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun x -> () : string -> unit) @@ -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 @@ -125,7 +151,7 @@ let call_linker ?(fatal=true) prefix f upds = if not (Sys.file_exists f) then begin let msg = "Cannot find native compiler file " ^ f in - if fatal then CErrors.error msg + if fatal then CErrors.user_err Pp.(str msg) else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else @@ -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 = |