From 1d8725b59309c2c9f870eb52a2daebe87ed9ad5b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Oct 2017 16:12:26 +0200 Subject: [flambda] [native] Pass `-Oclassic` to the native compiler. This seems a safe choice as of today, but more advanced users would like to tweak it, or we could even refine it by a configure option if desired. --- kernel/nativelib.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'kernel/nativelib.ml') diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 665ddf7a6..e9c0e171a 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -74,7 +74,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let remove f = if Sys.file_exists f then Sys.remove f in remove link_filename; remove (f ^ ".cmi"); - let initial_args = + let initial_args = if Dynlink.is_native then ["opt"; "-shared"] else @@ -86,9 +86,20 @@ let call_compiler ?profile:(profile=false) ml_filename = else [] in + let flambda_args = + if Coq_config.caml_version_nums >= [4;3;0] 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 = initial_args @ - profile_args @ + profile_args @ + flambda_args @ ("-o"::link_filename ::"-rectypes" ::"-w"::"a" -- cgit v1.2.3