diff options
| author | Guillaume Melquiond | 2021-02-12 16:56:55 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-26 08:16:34 +0100 |
| commit | 94319a520e7df0713942c2caada43214b49ed19b (patch) | |
| tree | c3f613e85c065b1ecfe6a5a37b8640969bcdc9a2 /kernel/nativelib.mli | |
| parent | 7b2cab92eb2d76f4768a2b0ff6d8ccf12102f101 (diff) | |
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.
Diffstat (limited to 'kernel/nativelib.mli')
| -rw-r--r-- | kernel/nativelib.mli | 26 |
1 files changed, 13 insertions, 13 deletions
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 |