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.

9 files changed, 20 insertions, 52 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 17c5a02e2b..914c951eb6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -104,7 +104,6 @@ type env = {
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
-  native_symbols : Nativevalues.symbols DPmap.t;
 }
 
 let empty_named_context_val = {
@@ -136,7 +135,6 @@ let empty_env = {
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab;
-  native_symbols = DPmap.empty;
 }
 
 
@@ -829,10 +827,6 @@ let is_type_in_type env r =
 
 let set_retroknowledge env r = { env with retroknowledge = r }
 
-let set_native_symbols env native_symbols = { env with native_symbols }
-let add_native_symbols dir syms env =
-  { env with native_symbols = DPmap.add dir syms env.native_symbols }
-
 module type QNameS =
 sig
   type t
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f0b40e6492..60696184ef 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -90,7 +90,6 @@ type env = private {
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
-  native_symbols : Nativevalues.symbols DPmap.t;
 }
 
 val oracle : env -> Conv_oracle.oracle
@@ -414,6 +413,3 @@ val no_link_info : link_info
 
 (** Primitives *)
 val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env
-
-val set_native_symbols : env -> Nativevalues.symbols DPmap.t -> env
-val add_native_symbols : DirPath.t -> Nativevalues.symbols -> env -> env
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index b5c4d6416a..911a879394 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2192,11 +2192,9 @@ let mk_norm_code env sigma prefix t =
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
-let mk_library_header dir =
-  let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
-  [Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_library_native_symbols"),
-    [|MLglobal (Ginternal libname)|]))]
+let mk_library_header (symbols : Nativevalues.symbols) =
+  let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in
+  [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
 
 let update_location (r,v) = r := v
 
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 71317d188b..913b3843c2 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -69,7 +69,7 @@ val compile_mind_field : ModPath.t -> Label.t ->
 val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code
 val mk_norm_code : env -> evars -> string -> constr -> linkable_code
 
-val mk_library_header : DirPath.t -> global list
+val mk_library_header : Nativevalues.symbols -> global list
 
 val mod_uid_of_dirpath : DirPath.t -> string
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 76215b4386..d77ee759c6 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -161,7 +161,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
   let fn = compile ml_filename code ~profile:false in
   if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
   let t0 = Sys.time () in
-  call_linker env ~fatal:true ~prefix fn (Some upds);
+  call_linker ~fatal:true ~prefix fn (Some upds);
   let t1 = Sys.time () in
   let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
   if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
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
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. *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3dee3d2b2f..bf02ceb2c2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -121,7 +121,6 @@ type compiled_library = {
   comp_univs : Univ.ContextSet.t;
   comp_deps : library_info array;
   comp_enga : engagement;
-  comp_natsymbs : Nativevalues.symbols
 }
 
 type reimport = compiled_library * Univ.ContextSet.t * vodigest
@@ -1139,7 +1138,6 @@ let end_module l restype senv =
   let mb, cst = build_module_body params restype senv in
   let senv = push_context_set ~strict:true (Univ.LSet.empty,cst) senv in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
-  let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
   let newenv = set_engagement_opt newenv senv.engagement in
   let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
   let senv' = propagate_loads { senv with env = newenv } in
@@ -1166,7 +1164,6 @@ let end_modtype l senv =
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
-  let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in
   let newenv = set_engagement_opt newenv senv.engagement in
   let newenv = Environ.set_universes (Environ.universes senv.env) newenv in
   let senv' = propagate_loads {senv with env=newenv} in
@@ -1229,8 +1226,6 @@ let module_of_library lib = lib.comp_mod
 
 let univs_of_library lib = lib.comp_univs
 
-type native_library = Nativecode.global list
-
 (** FIXME: MS: remove?*)
 let current_modpath senv = senv.modpath
 let current_dirpath senv = Names.ModPath.dp (current_modpath senv)
@@ -1272,9 +1267,8 @@ let export ?except ~output_native_objects senv dir =
     comp_univs = senv.univ;
     comp_deps = Array.of_list (DPmap.bindings senv.required);
     comp_enga = Environ.engagement senv.env;
-    comp_natsymbs = symbols }
-  in
-  mp, lib, ast
+  } in
+  mp, lib, (ast, symbols)
 
 (* cst are the constraints that were computed by the vi2vo step and hence are
  * not part of the [lib.comp_univs] field (but morally should be) *)
@@ -1294,7 +1288,6 @@ let import lib cst vodigest senv =
     let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in
     Modops.add_linked_module mb linkinfo env
   in
-  let env = Environ.add_native_symbols lib.comp_name lib.comp_natsymbs env in
   let sections =
     Option.map (Section.map_custom (fun custom ->
         {custom with rev_reimport = (lib,cst,vodigest) :: custom.rev_reimport}))
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b601279e87..6fa9022906 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -191,8 +191,6 @@ val current_dirpath : safe_environment -> DirPath.t
 
 type compiled_library
 
-type native_library = Nativecode.global list
-
 val module_of_library : compiled_library -> Declarations.module_body
 val univs_of_library : compiled_library -> Univ.ContextSet.t
 
@@ -201,7 +199,7 @@ val start_library : DirPath.t -> ModPath.t safe_transformer
 val export :
   ?except:Future.UUIDSet.t -> output_native_objects:bool ->
   safe_environment -> DirPath.t ->
-    ModPath.t * compiled_library * native_library
+    ModPath.t * compiled_library * Nativelib.native_library
 
 (* Constraints are non empty iff the file is a vi2vo *)
 val import : compiled_library -> Univ.ContextSet.t -> vodigest ->