Better error message when OCaml compiler not found for native compute

Fixes #6699

3 files changed, 22 insertions, 30 deletions

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index baa290367f..d153f84e9c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Names
 open Nativelib
 open Reduction
@@ -152,19 +151,15 @@ let native_conv_gen pb sigma env univs t1 t2 =
   else
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code env sigma prefix t1 t2 in
-  match compile ml_filename code ~profile:false with
-  | (true, fn) ->
-      begin
-        if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
-        let t0 = Sys.time () in
-        call_linker ~fatal:true prefix fn (Some upds);
-        let t1 = Sys.time () in
-        let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        (* TODO change 0 when we can have de Bruijn *)
-        fst (conv_val env pb 0 !rt1 !rt2 univs)
-      end
-  | _ -> anomaly (Pp.str "Compilation failure.") 
+  let fn = compile ml_filename code ~profile:false in
+  if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
+  let t0 = Sys.time () in
+  call_linker ~fatal:true prefix fn (Some upds);
+  let t1 = Sys.time () in
+  let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+  if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+  (* TODO change 0 when we can have de Bruijn *)
+  fst (conv_val env pb 0 !rt1 !rt2 univs)
 
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 833e4082f0..43c9676f05 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -56,14 +56,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
+let error_native_compiler_failed e =
+  let msg = match e with
+  | Inl (Unix.WEXITED 127) -> Pp.(strbrk "The OCaml compiler was not found. Make sure it is installed, together with findlib.")
   | 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
+  CErrors.user_err msg
 
 let call_compiler ?profile:(profile=false) ml_filename =
   let load_path = !get_load_paths () in
@@ -100,15 +101,12 @@ let call_compiler ?profile:(profile=false) ml_filename =
   if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (Envars.ocamlfind ()) args in
-    let res = match res with
-      | Unix.WEXITED 0 -> true
-      | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
-        warn_native_compiler_failed (Inl res); false
-    in
-    res, link_filename
+    match res with
+    | Unix.WEXITED 0 -> link_filename
+    | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
+      error_native_compiler_failed (Inl res)
   with Unix.Unix_error (e,_,_) ->
-    warn_native_compiler_failed (Inr e);
-    false, link_filename
+    error_native_compiler_failed (Inr e)
 
 let compile fn code ~profile:profile =
   write_ml_code fn code;
@@ -128,9 +126,8 @@ let compile_library dir code fn =
   in
   let fn = dirname / basename in
   write_ml_code fn ~header code;
-  let r = fst (call_compiler fn) in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
-  r
+  let _ = call_compiler fn in
+  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
 
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. *)
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 25adcf224b..d8557e667f 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,9 +21,9 @@ val load_obj : (string -> unit) ref
 
 val get_ml_filename : unit -> string * string
 
-val compile : string -> global list -> profile:bool -> bool * string
+val compile : string -> global list -> profile:bool -> string
 
-val compile_library : Names.DirPath.t -> global list -> string -> bool
+val compile_library : Names.DirPath.t -> global list -> string -> unit
 
 val call_linker :
   ?fatal:bool -> string -> string -> code_location_updates option -> unit