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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/declaremods.mli | 2 | ||||
| -rw-r--r-- | vernac/library.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index 9ca2ca5593..a1b98e4d9c 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -86,7 +86,7 @@ val start_library : library_name -> unit val end_library : ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name -> - Safe_typing.compiled_library * library_objects * Safe_typing.native_library + Safe_typing.compiled_library * library_objects * Nativelib.native_library (** append a function to be executed at end_library *) val append_end_library_hook : (unit -> unit) -> unit diff --git a/vernac/library.ml b/vernac/library.ml index e580927bfd..8a9b1fd68d 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -160,7 +160,7 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f + Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function | [] -> @@ -502,7 +502,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab = (* Writing native code files *) if output_native_objects then let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in - Nativelib.compile_library dir ast fn + Nativelib.compile_library ast fn let save_library_raw f sum lib univs proofs = save_library_base f sum lib (Some univs) None proofs |