Delay the dynamic linking of native-code libraries until native_compute is called (fix #13849).

The libraries are eventually linked in native_norm and native_conv_gen,
just before mk_norm_code and mk_conv_code are called.

This commit also renames call_linker as execute_library to better reflect
its role. It also makes link_library independent from it, since their
error handling are completely opposite.

1 files changed, 29 insertions, 20 deletions

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