diff options
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 |