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, 5 insertions, 9 deletions

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;