diff options
| author | Pierre-Marie Pédrot | 2020-11-02 15:37:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-09 16:38:46 +0100 |
| commit | fb5aa52ab8d870ee3613de325fbab7c98c33a433 (patch) | |
| tree | 2d3af63b32225f14a1c541c8fcabe0ed54a8fbfc /kernel/nativelib.mli | |
| parent | d2047c6368ae11a3a3fd7f2db8c991d135094e60 (diff) | |
Remove the native symbol registering from the safe environment.
Instead we store that data in the native code that was generated in adapt
the compilation scheme accordingly. Less indirections and less imperative
tinkering makes the code safer.
The global symbol table was originally introduced in #10359 as a way not to
depend on the Global module in the generated code. By storing all the
native-related information in the cmxs file itself, this PR also makes other
changes easier, such as e.g. #13287.
Diffstat (limited to 'kernel/nativelib.mli')
| -rw-r--r-- | kernel/nativelib.mli | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 29b4d20197..0c0fe3acc9 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -27,27 +27,24 @@ val get_ml_filename : unit -> string * string whether are in byte mode or not; file is expected to be .ml file *) val compile : string -> global list -> profile:bool -> string -(** [compile_library lib code file] is similar to [compile file code] +type native_library = Nativecode.global list * Nativevalues.symbols + +(** [compile_library (code, _) file] is similar to [compile file code] but will perform some extra tweaks to handle [code] as a Coq lib. *) -val compile_library : Names.DirPath.t -> global list -> string -> unit +val compile_library : native_library -> string -> unit val call_linker : ?fatal:bool - -> Environ.env -> prefix:string -> string -> code_location_updates option -> unit val link_library - : Environ.env - -> prefix:string + : prefix:string -> dirname:string -> basename:string -> unit val rt1 : Nativevalues.t ref val rt2 : Nativevalues.t ref - -val get_library_native_symbols : Names.DirPath.t -> Nativevalues.symbols -(** Strictly for usage by code produced by native compute. *) |