aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--lib/flags.ml3
-rw-r--r--lib/flags.mli3
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/declaremods.mli2
-rw-r--r--library/global.ml3
-rw-r--r--library/global.mli2
-rw-r--r--library/library.ml6
-rw-r--r--library/library.mli4
-rw-r--r--stm/stm.ml5
-rw-r--r--stm/stm.mli2
-rw-r--r--toplevel/ccompile.ml6
-rw-r--r--toplevel/coqargs.ml6
-rw-r--r--toplevel/coqargs.mli2
15 files changed, 29 insertions, 25 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 474ce3e871..18a257047d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1114,7 +1114,7 @@ let start_library dir senv =
modvariant = LIBRARY;
required = senv.required }
-let export ?except senv dir =
+let export ?except ~output_native_objects senv dir =
let senv =
try join_safe_environment ?except senv
with e ->
@@ -1136,7 +1136,7 @@ let export ?except senv dir =
}
in
let ast, symbols =
- if !Flags.output_native_objects then
+ if output_native_objects then
Nativelibrary.dump_library mp dir senv.env str
else [], Nativecode.empty_symbols
in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b7239da23..8539fdd504 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -187,7 +187,7 @@ val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.sym
val start_library : DirPath.t -> ModPath.t safe_transformer
val export :
- ?except:Future.UUIDSet.t ->
+ ?except:Future.UUIDSet.t -> output_native_objects:bool ->
safe_environment -> DirPath.t ->
ModPath.t * compiled_library * native_library
diff --git a/lib/flags.ml b/lib/flags.ml
index 29406ef275..7b1da2ff0e 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -118,8 +118,5 @@ let inline_level = ref default_inline_level
let set_inline_level = (:=) inline_level
let get_inline_level () = !inline_level
-(* Native code compilation for conversion and normalization *)
-let output_native_objects = ref false
-
let profile_ltac = ref false
let profile_ltac_cutoff = ref 2.0
diff --git a/lib/flags.mli b/lib/flags.mli
index b9c5e20f47..df9f464a14 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -112,9 +112,6 @@ val set_inline_level : int -> unit
val get_inline_level : unit -> int
val default_inline_level : int
-(** When producing vo objects, also compile the native-code version *)
-val output_native_objects : bool ref
-
(** Global profile_ltac flag *)
val profile_ltac : bool ref
val profile_ltac_cutoff : float ref
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8699583cdf..5fd11e187a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -928,10 +928,10 @@ let append_end_library_hook f =
let old_f = !end_library_hook in
end_library_hook := fun () -> old_f(); f ()
-let end_library ?except dir =
+let end_library ?except ~output_native_objects dir =
!end_library_hook();
let oname = Lib.end_compilation_checks dir in
- let mp,cenv,ast = Global.export ?except dir in
+ let mp,cenv,ast = Global.export ?except ~output_native_objects dir in
let prefix, lib_stack = Lib.end_compilation oname in
assert (ModPath.equal mp (MPfile dir));
let substitute, keep, _ = Lib.classify_segment lib_stack in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 7aa4bc30ce..2b28ba908e 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -99,7 +99,7 @@ val get_library_native_symbols : library_name -> Nativecode.symbols
val start_library : library_name -> unit
val end_library :
- ?except:Future.UUIDSet.t -> library_name ->
+ ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name ->
Safe_typing.compiled_library * library_objects * Safe_typing.native_library
(** append a function to be executed at end_library *)
diff --git a/library/global.ml b/library/global.ml
index 784a02449c..cf996ce644 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -143,7 +143,8 @@ let mind_of_delta_kn kn =
(** Operations on libraries *)
let start_library dir = globalize (Safe_typing.start_library dir)
-let export ?except s = Safe_typing.export ?except (safe_env ()) s
+let export ?except ~output_native_objects s =
+ Safe_typing.export ?except ~output_native_objects (safe_env ()) s
let import c u d = globalize (Safe_typing.import c u d)
diff --git a/library/global.mli b/library/global.mli
index df18625a5f..4e2ad92717 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -108,7 +108,7 @@ val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.
(** {6 Compiled libraries } *)
val start_library : DirPath.t -> ModPath.t
-val export : ?except:Future.UUIDSet.t -> DirPath.t ->
+val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t ->
ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
val import :
Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest ->
diff --git a/library/library.ml b/library/library.ml
index 9b9bd07c93..37dadadb76 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -657,7 +657,7 @@ let error_recursively_dependent_library dir =
(* Security weakness: file might have been changed on disk between
writing the content and computing the checksum... *)
-let save_library_to ?todo dir f otab =
+let save_library_to ?todo ~output_native_objects dir f otab =
let except = match todo with
| None ->
(* XXX *)
@@ -668,7 +668,7 @@ let save_library_to ?todo dir f otab =
assert(Filename.check_suffix f ".vio");
List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
Future.UUIDSet.empty l in
- let cenv, seg, ast = Declaremods.end_library ~except dir in
+ let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
let tasks, utab, dtab =
match todo with
@@ -716,7 +716,7 @@ let save_library_to ?todo dir f otab =
System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
(* Writing native code files *)
- if !Flags.output_native_objects then
+ if output_native_objects then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
user_err Pp.(str "Could not compile the library to native code.")
diff --git a/library/library.mli b/library/library.mli
index c016352808..a976be0184 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,9 +38,11 @@ type seg_proofs = Constr.constr Future.computation array
an export otherwise just a simple import *)
val import_module : bool -> qualid list -> unit
-(** End the compilation of a library and save it to a ".vo" file *)
+(** End the compilation of a library and save it to a ".vo" file.
+ [output_native_objects]: when producing vo objects, also compile the native-code version. *)
val save_library_to :
?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
+ output_native_objects:bool ->
DirPath.t -> string -> Opaqueproof.opaquetab -> unit
val load_library_todo :
diff --git a/stm/stm.ml b/stm/stm.ml
index 0165b3c029..5b13fc6a37 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2885,11 +2885,12 @@ let handle_failure (e, info) vcs =
VCS.print ();
Exninfo.iraise (e, info)
-let snapshot_vio ~doc ldir long_f_dot_vo =
+let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo =
let doc = finish ~doc in
if List.length (VCS.branches ()) > 1 then
CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
- Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
+ Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects
+ ldir long_f_dot_vo
(Global.opaque_tables ());
doc
diff --git a/stm/stm.mli b/stm/stm.mli
index 821ab59a43..91651e3534 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -156,7 +156,7 @@ val join : doc:doc -> doc
- if the worker proof is not empty, then it waits until all workers
are done with their current jobs and then dumps (or fails if one
of the completed tasks is a failure) *)
-val snapshot_vio : doc:doc -> DirPath.t -> string -> doc
+val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
(* Empties the task queue, can be used only if the worker pool is empty (E.g.
* after having built a .vio in batch mode *)
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index df2b983029..31656e0b07 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -125,7 +125,8 @@ let compile opts copts ~echo ~f_in ~f_out =
let _doc = Stm.join ~doc:state.doc in
let wall_clock2 = Unix.gettimeofday () in
check_pending_proofs ();
- Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
+ let output_native_objects = opts.output_native_objects in
+ Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
Aux_file.record_in_aux_at "vo_compile_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
@@ -168,7 +169,8 @@ let compile opts copts ~echo ~f_in ~f_out =
let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
let doc = Stm.finish ~doc:state.doc in
check_pending_proofs ();
- let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
+ let output_native_objects = opts.output_native_objects in
+ let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in
Stm.reset_task_queue ()
| Vio2Vo ->
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 74c016101a..25e9177b45 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -55,6 +55,7 @@ type t = {
indices_matter : bool;
enable_VM : bool;
enable_native_compiler : bool;
+ output_native_objects : bool;
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
@@ -100,6 +101,8 @@ let default = {
indices_matter = false;
enable_VM = true;
enable_native_compiler = Coq_config.native_compiler;
+ output_native_objects = false;
+
stm_flags = Stm.AsyncOpts.default_opts;
debug = false;
diffs_set = false;
@@ -421,8 +424,7 @@ let parse_args ~help ~init arglist : t * string list =
| ("no" | "off") -> false, false
| _ -> prerr_endline ("Error: (yes|no|ondemand) expected after option -native-compiler"); exit 1
in
- Flags.output_native_objects := precompile;
- { oval with enable_native_compiler = enable }
+ { oval with output_native_objects = precompile; enable_native_compiler = enable }
(* Options with zero arg *)
|"-async-queries-always-delegate"
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index c9a7a0fd56..c603505f8c 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -33,6 +33,8 @@ type t = {
indices_matter : bool;
enable_VM : bool;
enable_native_compiler : bool;
+ output_native_objects : bool;
+
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
diffs_set : bool;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:36:45 +0000