aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/values.ml2
-rw-r--r--kernel/environ.ml6
-rw-r--r--kernel/environ.mli4
-rw-r--r--kernel/nativecode.ml8
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativeconv.ml2
-rw-r--r--kernel/nativelib.ml22
-rw-r--r--kernel/nativelib.mli13
-rw-r--r--kernel/safe_typing.ml11
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--library/global.mli2
-rw-r--r--pretyping/nativenorm.ml2
-rw-r--r--vernac/declaremods.mli2
-rw-r--r--vernac/library.ml4
14 files changed, 26 insertions, 58 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 38cb243f80..4e99d087df 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -374,7 +374,7 @@ and v_modtype =
let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
let v_compiled_lib =
- v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps;v_engagement;Any|]
+ v_tuple "compiled" [|v_dp;v_module;v_context_set;v_deps;v_engagement|]
(** Library objects *)
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 ->
diff --git a/library/global.mli b/library/global.mli
index 2767594171..5faf0e8bbd 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -134,7 +134,7 @@ val body_of_constant_body : Opaqueproof.indirect_accessor ->
val start_library : DirPath.t -> ModPath.t
val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t ->
- ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
+ ModPath.t * Safe_typing.compiled_library * Nativelib.native_library
val import :
Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest ->
ModPath.t
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 3f68e3c78f..d06d6e01d1 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -525,7 +525,7 @@ let native_norm env sigma c ty =
if print_timing then Feedback.msg_info (Pp.str time_info);
let profiler_pid = if profile then start_profiler () else None in
let t0 = Unix.gettimeofday () in
- Nativelib.call_linker ~fatal:true env ~prefix fn (Some upd);
+ Nativelib.call_linker ~fatal:true ~prefix fn (Some upd);
let t1 = Unix.gettimeofday () in
if profile then stop_profiler profiler_pid;
let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:15:26 +0000