aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/01-kernel/13853-delay-native.rst6
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativeconv.ml22
-rw-r--r--kernel/nativelib.ml49
-rw-r--r--kernel/nativelib.mli26
-rw-r--r--pretyping/nativenorm.ml17
-rw-r--r--vernac/library.ml14
7 files changed, 75 insertions, 61 deletions
diff --git a/doc/changelog/01-kernel/13853-delay-native.rst b/doc/changelog/01-kernel/13853-delay-native.rst
new file mode 100644
index 0000000000..59bf960a0f
--- /dev/null
+++ b/doc/changelog/01-kernel/13853-delay-native.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+ Native-code libraries used by :tacn:`native_compute` are now delayed
+ until an actual call to the :tacn:`native_compute` machinery is
+ performed. This should make Coq more responsive on some systems
+ (`#13853 <https://github.com/coq/coq/pull/13853>`_, fixes `#13849
+ <https://github.com/coq/coq/issues/13849>`_, by Guillaume Melquiond).
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 1b14801fec..90525a19b2 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -63,6 +63,8 @@ val empty_updates : code_location_updates
val register_native_file : string -> unit
+val is_loaded_native_file : string -> bool
+
val compile_constant_field : env -> string -> Constant.t ->
global list -> 'a constant_body -> global list
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 7e73725c6c..f0ae5e2fbf 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Nativelib
open Reduction
open Util
open Nativevalues
@@ -151,22 +150,25 @@ let warn_no_native_compiler =
strbrk " falling back to VM conversion test.")
let native_conv_gen pb sigma env univs t1 t2 =
- if not (typing_flags env).Declarations.enable_native_compiler then begin
- warn_no_native_compiler ();
- Vconv.vm_conv_gen pb env univs t1 t2
- end
- else
- let ml_filename, prefix = get_ml_filename () in
+ Nativelib.link_libraries ();
+ let ml_filename, prefix = Nativelib.get_ml_filename () in
let code, upds = mk_conv_code env sigma prefix t1 t2 in
- let fn = compile ml_filename code ~profile:false in
+ let fn = Nativelib.compile ml_filename code ~profile:false in
debug_native_compiler (fun () -> Pp.str "Running test...");
let t0 = Sys.time () in
- call_linker ~fatal:true ~prefix fn (Some upds);
+ let (rt1, rt2) = Nativelib.execute_library ~prefix fn upds in
let t1 = Sys.time () in
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
debug_native_compiler (fun () -> Pp.str time_info);
(* TODO change 0 when we can have de Bruijn *)
- fst (conv_val env pb 0 !rt1 !rt2 univs)
+ fst (conv_val env pb 0 rt1 rt2 univs)
+
+let native_conv_gen pb sigma env univs t1 t2 =
+ if not (typing_flags env).Declarations.enable_native_compiler then begin
+ warn_no_native_compiler ();
+ Vconv.vm_conv_gen pb env univs t1 t2
+ end
+ else native_conv_gen pb sigma env univs t1 t2
(* 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 3eb3c949bc..73567e34cf 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -162,32 +162,41 @@ let compile_library (code, symb) fn =
let _ = call_compiler fn in
if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn
-(* call_linker links dynamically the code for constants in environment or a *)
-(* conversion test. *)
-let call_linker ?(fatal=true) ~prefix f upds =
+let execute_library ~prefix f upds =
rt1 := dummy_value ();
rt2 := dummy_value ();
if not (Sys.file_exists f) then
- begin
- let msg = "Cannot find native compiler file " ^ f in
- if fatal then CErrors.user_err Pp.(str msg)
- else debug_native_compiler (fun () -> 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 _ as exn ->
- let exn = Exninfo.capture exn in
- if fatal then Exninfo.iraise exn
- else debug_native_compiler (fun () -> CErrors.(iprint exn)));
- match upds with Some upds -> update_locations upds | _ -> ()
-
-let link_library ~prefix ~dirname ~basename =
+ CErrors.user_err Pp.(str "Cannot find native compiler file " ++ str f);
+ if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
+ register_native_file prefix;
+ update_locations upds;
+ (!rt1, !rt2)
+
+let link_library dirname prefix =
+ let basename = Dynlink.adapt_filename (prefix ^ "cmo") in
(* We try both [output_dir] and [.coq-native], unfortunately from
[Require] we don't know if we are loading a library in the build
dir or in the installed layout *)
let install_location = dirname / dft_output_dir / basename in
let build_location = dirname / !output_dir / basename in
let f = if Sys.file_exists build_location then build_location else install_location in
- call_linker ~fatal:false ~prefix f None
+ try
+ if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
+ register_native_file prefix
+ with
+ | Dynlink.Error _ as exn ->
+ debug_native_compiler (fun () -> CErrors.iprint (Exninfo.capture exn))
+
+let delayed_link = ref []
+
+let link_libraries () =
+ let delayed = List.rev !delayed_link in
+ delayed_link := [];
+ List.iter (fun (dirname, libname) ->
+ let prefix = mod_uid_of_dirpath libname ^ "." in
+ if not (Nativecode.is_loaded_native_file prefix) then
+ link_library dirname prefix
+ ) delayed
+
+let enable_library dirname libname =
+ delayed_link := (dirname, libname) :: !delayed_link
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 0c0fe3acc9..ba04c28ab0 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -7,7 +7,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Nativecode
(** This file provides facilities to access OCaml compiler and dynamic linker,
used by the native compiler. *)
@@ -25,7 +24,7 @@ val get_ml_filename : unit -> string * string
(** [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
+val compile : string -> Nativecode.global list -> profile:bool -> string
type native_library = Nativecode.global list * Nativevalues.symbols
@@ -33,18 +32,19 @@ type native_library = Nativecode.global list * Nativevalues.symbols
but will perform some extra tweaks to handle [code] as a Coq lib. *)
val compile_library : native_library -> string -> unit
-val call_linker
- : ?fatal:bool
- -> prefix:string
- -> string
- -> code_location_updates option
- -> unit
+(** [execute_library file upds] dynamically loads library [file],
+ updates the library locations [upds], and returns the values stored
+ in [rt1] and [rt2] *)
+val execute_library :
+ prefix:string -> string -> Nativecode.code_location_updates ->
+ Nativevalues.t * Nativevalues.t
-val link_library
- : prefix:string
- -> dirname:string
- -> basename:string
- -> unit
+(** [enable_library] marks the given library for dynamic loading
+ the next time [link_libraries] is called. *)
+val enable_library : string -> Names.DirPath.t -> unit
+val link_libraries : unit -> unit
+
+(* used for communication with the loaded libraries *)
val rt1 : Nativevalues.t ref
val rt2 : Nativevalues.t ref
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 28621aa92e..2c107502f4 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -502,15 +502,9 @@ let stop_profiler m_pid =
| _ -> ()
let native_norm env sigma c ty =
+ Nativelib.link_libraries ();
let c = EConstr.Unsafe.to_constr c in
let ty = EConstr.Unsafe.to_constr ty in
- if not (Flags.get_native_compiler ()) then
- user_err Pp.(str "Native_compute reduction has been disabled.")
- else
- (*
- 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 profile = get_profiling_enabled () in
let print_timing = get_timing_enabled () in
let ml_filename, prefix = Nativelib.get_ml_filename () in
@@ -526,17 +520,22 @@ let native_norm env sigma c ty =
if print_timing then Feedback.msg_info (Pp.str time_info);
let profiler_pid = if profile then start_profiler () else None in
let t0 = Unix.gettimeofday () in
- Nativelib.call_linker ~fatal:true ~prefix fn (Some upd);
+ let (rt1, _) = Nativelib.execute_library ~prefix fn upd in
let t1 = Unix.gettimeofday () in
if profile then stop_profiler profiler_pid;
let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in
if print_timing then Feedback.msg_info (Pp.str time_info);
- let res = nf_val env sigma !Nativelib.rt1 ty in
+ let res = nf_val env sigma rt1 ty in
let t2 = Unix.gettimeofday () in
let time_info = Format.sprintf "native_compute: Reification done in %.5f" (t2 -. t1) in
if print_timing then Feedback.msg_info (Pp.str time_info);
EConstr.of_constr res
+let native_norm env sigma c ty =
+ if not (Flags.get_native_compiler ()) then
+ user_err Pp.(str "Native_compute reduction has been disabled.");
+ native_norm env sigma c ty
+
let native_conv_generic pb sigma t =
Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
diff --git a/vernac/library.ml b/vernac/library.ml
index 8a9b1fd68d..cc9e3c3c44 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -155,17 +155,13 @@ let library_is_loaded dir =
let register_loaded_library m =
let libname = m.libsum_name in
- let link () =
- let dirname = Filename.dirname (library_full_filename libname) in
- let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
- let f = prefix ^ "cmo" in
- let f = Dynlink.adapt_filename f in
- Nativelib.link_library ~prefix ~dirname ~basename:f
- in
let rec aux = function
| [] ->
- let () = if Flags.get_native_compiler () then link () in
- [libname]
+ if Flags.get_native_compiler () then begin
+ let dirname = Filename.dirname (library_full_filename libname) in
+ Nativelib.enable_library dirname libname
+ end;
+ [libname]
| m'::_ as l when DirPath.equal m' libname -> l
| m'::l' -> m' :: aux l' in
libraries_loaded_list := aux !libraries_loaded_list;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:27:17 +0000