Merge PR #13853: Delay the dynamic linking of native-code libraries until native_compute is called.

Ack-by: ejgallego
Reviewed-by: ppedrot

4 files changed, 56 insertions, 43 deletions

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