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

Ack-by: ejgallego
Reviewed-by: ppedrot

1 files changed, 12 insertions, 10 deletions

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 =