[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.

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"