diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-09 16:12:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-10 10:47:58 +0200 |
| commit | 1d8725b59309c2c9f870eb52a2daebe87ed9ad5b (patch) | |
| tree | 5f7beb8ea5b420cbbcbad414e6f216b34d08b464 /kernel/nativelib.ml | |
| parent | 406717ce786a70e64b9043db45dd5a2add68f817 (diff) | |
[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.
Diffstat (limited to 'kernel/nativelib.ml')
| -rw-r--r-- | kernel/nativelib.ml | 15 |
1 files changed, 13 insertions, 2 deletions
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" |