aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml29
-rw-r--r--checker/check.mli5
-rw-r--r--checker/check_stat.ml4
-rw-r--r--checker/check_stat.mli3
-rw-r--r--checker/checker.ml51
-rw-r--r--checker/mod_checking.ml2
-rw-r--r--checker/safe_checking.ml11
-rw-r--r--checker/safe_checking.mli4
8 files changed, 59 insertions, 50 deletions
diff --git a/checker/check.ml b/checker/check.ml
index f37dde263a..e3a4bda8ec 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -111,21 +111,23 @@ let () =
Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table
-let check_one_lib admit (dir,m) =
+let check_one_lib admit senv (dir,m) =
let md = m.library_compiled in
let dig = m.library_digest in
(* Look up if the library is to be admitted correct. We could
also check if it carries a validation certificate (yet to
be implemented). *)
- if LibrarySet.mem dir admit then
- (Flags.if_verbose Feedback.msg_notice
- (str "Admitting library: " ++ pr_dirpath dir);
- Safe_checking.unsafe_import md m.library_extra_univs dig)
- else
- (Flags.if_verbose Feedback.msg_notice
- (str "Checking library: " ++ pr_dirpath dir);
- Safe_checking.import md m.library_extra_univs dig);
- register_loaded_library m
+ let senv =
+ if LibrarySet.mem dir admit then
+ (Flags.if_verbose Feedback.msg_notice
+ (str "Admitting library: " ++ pr_dirpath dir);
+ Safe_checking.unsafe_import senv md m.library_extra_univs dig)
+ else
+ (Flags.if_verbose Feedback.msg_notice
+ (str "Checking library: " ++ pr_dirpath dir);
+ Safe_checking.import senv md m.library_extra_univs dig)
+ in
+ register_loaded_library m; senv
(*************************************************************************)
(*s Load path. Mapping from physical to logical paths etc.*)
@@ -423,7 +425,7 @@ and fold_deps_list seen ff modl needed =
let fold_deps_list ff modl acc =
snd (fold_deps_list LibrarySet.empty ff modl (LibrarySet.empty,acc))
-let recheck_library ~norec ~admit ~check =
+let recheck_library senv ~norec ~admit ~check =
let ml = List.map try_locate_qualified_library check in
let nrl = List.map try_locate_qualified_library norec in
let al = List.map try_locate_qualified_library admit in
@@ -441,5 +443,6 @@ let recheck_library ~norec ~admit ~check =
Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
prlist
(fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
- List.iter (check_one_lib nochk) needed;
- Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
+ let senv = List.fold_left (check_one_lib nochk) senv needed in
+ Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked");
+ senv
diff --git a/checker/check.mli b/checker/check.mli
index eb6404a172..39cc93c060 100644
--- a/checker/check.mli
+++ b/checker/check.mli
@@ -10,6 +10,7 @@
open CUnix
open Names
+open Safe_typing
type section_path = {
dirpath : string list;
@@ -26,7 +27,7 @@ val default_root_prefix : DirPath.t
val add_load_path : physical_path * logical_path -> unit
-val recheck_library :
+val recheck_library : safe_environment ->
norec:object_file list ->
admit:object_file list ->
- check:object_file list -> unit
+ check:object_file list -> safe_environment
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index ddee1eda8f..588fb8e8b1 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -65,6 +65,6 @@ let print_context env = () (* FIXME
str "* " ++ hov 0 (pr_ax csts)));
end *)
-let stats () =
- print_context (Global.env());
+let stats senv =
+ print_context senv;
print_memory_stat ()
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index 823b107f5b..0cda7f0c8a 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -7,8 +7,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Safe_typing
val memory_stat : bool ref
val output_context : bool ref
-val stats : unit -> unit
+val stats : safe_environment -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
index 49f6bf185a..06c1e053d5 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,7 +138,11 @@ let set_debug () = Flags.debug := true
let impredicative_set = ref Declarations.PredicativeSet
let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet
-let engage () = Global.set_engagement (!impredicative_set)
+let engage = Safe_typing.set_engagement (!impredicative_set)
+
+let disable_compilers senv =
+ let senv = Safe_typing.set_VM false senv in
+ Safe_typing.set_native_compiler false senv
let admit_list = ref ([] : object_file list)
@@ -157,8 +161,8 @@ let add_compile s =
We no longer use [Arg.parse], in order to use share [Usage.print_usage]
between coqtop and coqc. *)
-let compile_files () =
- Check.recheck_library
+let compile_files senv =
+ Check.recheck_library senv
~norec:(List.rev !norec_list)
~admit:(List.rev !admit_list)
~check:(List.rev !compile_list)
@@ -362,35 +366,34 @@ let parse_args argv =
parse (List.tl (Array.to_list argv))
-(* To prevent from doing the initialization twice *)
-let initialized = ref false
-
(* XXX: At some point we need to either port the checker to use the
feedback system or to remove its use completely. *)
let init_with_argv argv =
- if not !initialized then begin
- initialized := true;
- Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
- let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
- try
- parse_args argv;
- if !Flags.debug then Printexc.record_backtrace true;
- Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
- Flags.if_verbose print_header ();
- init_load_path ();
- engage ();
- with e ->
- fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e)
- end
+ Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+ let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
+ try
+ parse_args argv;
+ if !Flags.debug then Printexc.record_backtrace true;
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
+ Flags.if_verbose print_header ();
+ init_load_path ();
+ let senv = Safe_typing.empty_environment in
+ disable_compilers (engage senv)
+ with e ->
+ fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e)
let init() = init_with_argv Sys.argv
-let run () =
+let run senv =
try
- compile_files ();
- flush_all()
+ let senv = compile_files senv in
+ flush_all(); senv
with e ->
if !Flags.debug then Printexc.print_backtrace stderr;
fatal_error (explain_exn e) (is_anomaly e)
-let start () = init(); run(); Check_stat.stats(); exit 0
+let start () =
+ let senv = init() in
+ let senv = run senv in
+ Check_stat.stats senv;
+ exit 0
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 94e7c29201..ed617d73c2 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -25,7 +25,7 @@ let check_constant_declaration env kn cb =
let ty = cb.const_type in
let _ = infer_type env' ty in
let () =
- match Global.body_of_constant_body cb with
+ match Environ.body_of_constant_body env cb with
| Some bd ->
let j = infer env' (fst bd) in
conv_leq env' j.uj_type ty
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
index 90b5188d26..6dc2953060 100644
--- a/checker/safe_checking.ml
+++ b/checker/safe_checking.ml
@@ -11,12 +11,13 @@
open Declarations
open Environ
-let import clib univs digest =
+let import senv clib univs digest =
let mb = Safe_typing.module_of_library clib in
- let env = push_context_set ~strict:true mb.mod_constraints (Global.env ()) in
+ let env = Safe_typing.env_of_safe_env senv in
+ let env = push_context_set ~strict:true mb.mod_constraints env in
let env = push_context_set ~strict:true univs env in
Mod_checking.check_module env mb.mod_mp mb;
- let _ = Global.import clib univs digest in ()
+ let (_,senv) = Safe_typing.import clib univs digest senv in senv
-let unsafe_import clib univs digest =
- let _ = Global.import clib univs digest in ()
+let unsafe_import senv clib univs digest =
+ let (_,senv) = Safe_typing.import clib univs digest senv in senv
diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli
index 75b1eab429..44cd2b3a2e 100644
--- a/checker/safe_checking.mli
+++ b/checker/safe_checking.mli
@@ -12,5 +12,5 @@
open Safe_typing
(*i*)
-val import : compiled_library -> Univ.ContextSet.t -> vodigest -> unit
-val unsafe_import : compiled_library -> Univ.ContextSet.t -> vodigest -> unit
+val import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment
+val unsafe_import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:26:53 +0000