From 94319a520e7df0713942c2caada43214b49ed19b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 12 Feb 2021 16:56:55 +0100
Subject: 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.
---
 kernel/nativelib.mli | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'kernel/nativelib.mli')

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
-- 
cgit v1.2.3