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.

1 files changed, 7 insertions, 15 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index c1f14923fa..1e1085d5ff 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -145,8 +145,10 @@ let compile fn code ~profile:profile =
   if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
   r
 
-let compile_library dir code fn =
-  let header = mk_library_header dir in
+type native_library = Nativecode.global list * Nativevalues.symbols
+
+let compile_library (code, symb) fn =
+  let header = mk_library_header symb in
   let fn = fn ^ source_ext in
   let basename = Filename.basename fn in
   let dirname = Filename.dirname fn in
@@ -160,19 +162,9 @@ let compile_library dir code fn =
   let _ = call_compiler fn in
   if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
 
-let native_symbols = ref Names.DPmap.empty
-
-let get_library_native_symbols dir =
-  try Names.DPmap.find dir !native_symbols
-  with Not_found ->
-    CErrors.user_err ~hdr:"get_library_native_symbols"
-      Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++
-          (str "This use case is not supported, but disabling the native compiler may help."))
-
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. *)
-let call_linker ?(fatal=true) env ~prefix f upds =
-  native_symbols := env.Environ.native_symbols;
+let call_linker ?(fatal=true) ~prefix f upds =
   rt1 := dummy_value ();
   rt2 := dummy_value ();
   if not (Sys.file_exists f) then
@@ -191,11 +183,11 @@ let call_linker ?(fatal=true) env ~prefix f upds =
      else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
   match upds with Some upds -> update_locations upds | _ -> ()
 
-let link_library env ~prefix ~dirname ~basename =
+let link_library ~prefix ~dirname ~basename =
   (* We try both [output_dir] and [.coq-native], unfortunately from
      [Require] we don't know if we are loading a library in the build
      dir or in the installed layout *)
   let install_location = dirname / dft_output_dir / basename in
   let build_location = dirname / !output_dir / basename in
   let f = if Sys.file_exists build_location then build_location else install_location in
-  call_linker env ~fatal:false ~prefix f None
+  call_linker ~fatal:false ~prefix f None