diff options
| -rw-r--r-- | kernel/nativeconv.ml | 23 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 25 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 11 | ||||
| -rw-r--r-- | library/library.ml | 3 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 36 |
5 files changed, 46 insertions, 52 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..e113350368 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -21,9 +21,14 @@ val load_obj : (string -> unit) ref val get_ml_filename : unit -> string * string -val compile : string -> global list -> profile:bool -> bool * string - -val compile_library : Names.DirPath.t -> global list -> string -> bool +(** [compile file code ~profile] will compile native [code] to [file], + and return the name of the object file; this name depends on + whether are in byte mode or not; file is expected to be .ml file *) +val compile : string -> global list -> profile:bool -> string + +(** [compile_library lib code file] is similar to [compile file code] + but will perform some extra tweaks to handle [code] as a Coq lib. *) +val compile_library : Names.DirPath.t -> global list -> string -> unit val call_linker : ?fatal:bool -> string -> string -> code_location_updates option -> unit diff --git a/library/library.ml b/library/library.ml index 37dadadb76..04e38296d9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -718,8 +718,7 @@ let save_library_to ?todo ~output_native_objects dir f otab = (* Writing native code files *) if output_native_objects then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in - if not (Nativelib.compile_library dir ast fn) then - user_err Pp.(str "Could not compile the library to native code.") + Nativelib.compile_library dir ast fn with reraise -> let reraise = CErrors.push reraise in let () = Feedback.msg_warning (str "Removed file " ++ str f') in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0003fc7280..e694502231 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -492,25 +492,23 @@ let native_norm env sigma c ty = Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); *) - let ml_filename, prefix = Nativelib.get_ml_filename () in - let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in - let profile = get_profiling_enabled () in - match Nativelib.compile ml_filename code ~profile:profile with - | true, fn -> - if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); - let profiler_pid = if profile then start_profiler () else None in - let t0 = Sys.time () in - Nativelib.call_linker ~fatal:true prefix fn (Some upd); - let t1 = Sys.time () in - if profile then stop_profiler profiler_pid; - let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); - let res = nf_val env sigma !Nativelib.rt1 ty in - let t2 = Sys.time () in - let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); - EConstr.of_constr res - | _ -> anomaly (Pp.str "Compilation failure.") + let ml_filename, prefix = Nativelib.get_ml_filename () in + let code, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in + let profile = get_profiling_enabled () in + let fn = Nativelib.compile ml_filename code ~profile:profile in + if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ..."); + let profiler_pid = if profile then start_profiler () else None in + let t0 = Sys.time () in + Nativelib.call_linker ~fatal:true prefix fn (Some upd); + let t1 = Sys.time () in + if profile then stop_profiler profiler_pid; + let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in + if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + let res = nf_val env sigma !Nativelib.rt1 ty in + let t2 = Sys.time () in + let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in + if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + EConstr.of_constr res let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t |