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. --- INSTALL | 12 +++++++----- config/coq_config.mli | 1 + configure.ml | 5 +++-- kernel/nativelib.ml | 15 +++++++++++++-- 4 files changed, 24 insertions(+), 9 deletions(-) diff --git a/INSTALL b/INSTALL index 808e76882..faac79f18 100644 --- a/INSTALL +++ b/INSTALL @@ -139,12 +139,14 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). of flags. You can read more at https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html - Note that a regular build with a flambda-enabled compiler - requires a large amount of RAM (>= 10GiB) in one particular - file, see: https://caml.inria.fr/mantis/view.php?id=7630 + There is a known problem with certain OCaml versions and + `native_compute`, that will make compilation to require + a large amount of RAM (>= 10GiB) in some particular files. - Meanwhile, users with less powerful machines are recommended - to disable native compilation with `-native-compiler no`. + We recommend disabling native compilation (`-native-compiler no`) + with flambda unless you use a modern (>= 4.06.0) OCaml. + + c.f. https://caml.inria.fr/mantis/view.php?id=7630 5- Still in the root directory, do diff --git a/config/coq_config.mli b/config/coq_config.mli index 885b3ef4c..8bc044c3a 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -49,6 +49,7 @@ val vmbyteflags : string list (* -custom/-dllib -lcoqrun *) val version : string (* version number of Coq *) val caml_version : string (* OCaml version used to compile Coq *) +val caml_version_nums : int list (* OCaml version used to compile Coq by components *) val date : string (* release date *) val compile_date : string (* compile date *) val vo_magic_number : int diff --git a/configure.ml b/configure.ml index 3ba1986c0..ca7979fa1 100644 --- a/configure.ml +++ b/configure.ml @@ -1028,8 +1028,8 @@ let write_configml f = let pr_i = pr "let %s = %d\n" in let pr_p s o = pr "let %s = %S\n" s (match o with Relative s -> s | Absolute s -> s) in - let pr_l n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l)) - in + let pr_l n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l)) in + let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; pr "(* Exact command that generated this file: *)\n"; pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); @@ -1059,6 +1059,7 @@ let write_configml f = pr_s "osdeplibs" osdeplibs; pr_s "version" coq_version; pr_s "caml_version" caml_version; + pr_li "caml_version_nums" caml_version_nums; pr_s "date" short_date; pr_s "compile_date" full_date; pr_s "arch" arch; 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