From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/nativelib.ml | 65 ++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 45 insertions(+), 20 deletions(-)

(limited to 'kernel/nativelib.ml')

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 =
-- 
cgit v1.2.3