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.ml7
-rw-r--r--toplevel/coqargs.ml23
-rw-r--r--toplevel/coqargs.mli5
-rw-r--r--toplevel/coqtop.ml2
16 files changed, 44 insertions, 33 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 9e0d7ed380..768d359cce 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -116,8 +116,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 1066f31a8b..4ef5fb4445 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -110,9 +110,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 e7833f253e..b4f26570c6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2890,11 +2890,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 313ac58111..102e832d3e 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -160,7 +160,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 ecb0407f75..8064ee8880 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -96,6 +96,9 @@ let compile opts copts ~echo ~f_in ~f_out =
let iload_path = build_load_path opts in
let require_libs = require_libs opts in
let stm_options = opts.stm_flags in
+ let output_native_objects = match opts.native_compiler with
+ | NativeOff -> false | NativeOn {ondemand} -> not ondemand
+ in
match copts.compilation_mode with
| BuildVo ->
Flags.record_aux_file := true;
@@ -126,7 +129,7 @@ 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 ());
+ 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 ();
@@ -170,7 +173,7 @@ 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 () = 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 ae3c5b32dc..b549f22119 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -33,6 +33,8 @@ let set_type_in_type () =
type color = [`ON | `AUTO | `OFF]
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
type t = {
boot : bool;
@@ -56,7 +58,7 @@ type t = {
impredicative_set : Declarations.set_predicativity;
indices_matter : bool;
enable_VM : bool;
- enable_native_compiler : bool;
+ native_compiler : native_compiler;
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
@@ -81,6 +83,11 @@ type t = {
let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
+let default_native =
+ if Coq_config.native_compiler
+ then NativeOn {ondemand=true}
+ else NativeOff
+
let default = {
boot = false;
@@ -103,7 +110,8 @@ let default = {
impredicative_set = Declarations.PredicativeSet;
indices_matter = false;
enable_VM = true;
- enable_native_compiler = Coq_config.native_compiler;
+ native_compiler = default_native;
+
stm_flags = Stm.AsyncOpts.default_opts;
debug = false;
diffs_set = false;
@@ -418,15 +426,14 @@ let parse_args ~help ~init arglist : t * string list =
produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by
a separate flag, and the "ondemand" value removed. Once this is done, use
[get_bool] here. *)
- let (enable,precompile) =
+ let native_compiler =
match (next ()) with
- | ("yes" | "on") -> true, true
- | "ondemand" -> true, false
- | ("no" | "off") -> false, false
+ | ("yes" | "on") -> NativeOn {ondemand=false}
+ | "ondemand" -> NativeOn {ondemand=true}
+ | ("no" | "off") -> NativeOff
| _ -> 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 native_compiler }
(* Options with zero arg *)
|"-async-queries-always-delegate"
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 52ab2b60d7..9cc846edea 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -12,6 +12,8 @@ type color = [`ON | `AUTO | `OFF]
val default_toplevel : Names.DirPath.t
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
type t = {
boot : bool;
@@ -34,7 +36,8 @@ type t = {
impredicative_set : Declarations.set_predicativity;
indices_matter : bool;
enable_VM : bool;
- enable_native_compiler : bool;
+ native_compiler : native_compiler;
+
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
diffs_set : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index faf26a9665..c2c538edea 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -188,7 +188,7 @@ let init_toplevel ~help ~init custom_init arglist =
Global.set_engagement opts.impredicative_set;
Global.set_indices_matter opts.indices_matter;
Global.set_VM opts.enable_VM;
- Global.set_native_compiler opts.enable_native_compiler;
+ Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
(* Allow the user to load an arbitrary state here *)
inputstate opts;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:55:54 +0000