From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

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

(limited to 'kernel/nativelib.ml')

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 948989fd..1c58c744 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -8,7 +8,7 @@
 open Util
 open Nativevalues
 open Nativecode
-open Errors
+open CErrors
 open Envars
 
 (** This file provides facilities to access OCaml compiler and dynamic linker,
@@ -30,10 +30,6 @@ let output_dir = ".coq-native"
 (* Extension of genereted ml files, stored for debugging purposes *)
 let source_ext = ".native"
 
-(* Global settings and utilies for interface with OCaml *)
-let compiler_name =
-  if Dynlink.is_native then ocamlopt () else ocamlc ()
-
 let ( / ) = Filename.concat
 
 (* We have to delay evaluation of include_dirs because coqlib cannot be guessed
@@ -59,6 +55,15 @@ let write_ml_code fn ?(header=[]) code =
   List.iter (pp_global fmt) (header@code);
   close_out ch_out
 
+let warn_native_compiler_failed =
+  let print = function
+  | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
+  | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
+  | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
+  | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
+  in
+  CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
+
 let call_compiler ml_filename =
   let load_path = !get_load_paths () in
   let load_path = List.map (fun dn -> dn / output_dir) load_path in
@@ -70,26 +75,24 @@ let call_compiler ml_filename =
   remove link_filename;
   remove (f ^ ".cmi");
   let args =
-    (if Dynlink.is_native then "-shared" else "-c")
+    (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
-  if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args)));
+  if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
   try
-    let res = CUnix.sys_command compiler_name args in
+    let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
-      | Unix.WEXITED n ->
-         Pp.(msg_warning (str "command exited with status " ++ int n)); false
-      | Unix.WSIGNALED n ->
-         Pp.(msg_warning (str "command killed by signal " ++ int n)); false
-      | Unix.WSTOPPED n ->
-         Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+        warn_native_compiler_failed (Inl res); false
+    in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    Pp.(msg_warning (str (Unix.error_message e)));
+    warn_native_compiler_failed (Inr e);
     false, link_filename
 
 let compile fn code =
@@ -122,18 +125,18 @@ 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 Errors.error msg
-      else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+      if fatal then CErrors.error msg
+      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
     end
   else
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
    with Dynlink.Error e as exn ->
-     let exn = Errors.push exn in
+     let exn = CErrors.push exn in
      let msg = "Dynlink error, " ^ Dynlink.error_message e in
-     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
-     else if !Flags.debug then Pp.msg_debug (Pp.str msg));
+     if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
+     else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
-- 
cgit v1.2.3