diff options
| author | Pierre-Marie Pédrot | 2021-02-28 12:58:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-02-28 12:58:44 +0100 |
| commit | ef22a5aaf1728d840341d31befd67dd90c5b2e0e (patch) | |
| tree | 1090422c9d0d9b8ae16c9ff2083dcf56f2668250 /kernel/nativelib.mli | |
| parent | 7b326354b32868750b3e3ce99b8dc9a3377909ba (diff) | |
| parent | 94319a520e7df0713942c2caada43214b49ed19b (diff) | |
Merge PR #13853: Delay the dynamic linking of native-code libraries until native_compute is called.
Ack-by: ejgallego
Reviewed-by: ppedrot
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 |