aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES.md14
-rw-r--r--checker/cic.mli2
-rw-r--r--checker/values.ml4
-rw-r--r--configure.ml2
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/nativeconv.ml5
-rw-r--r--kernel/nativelib.ml1
-rw-r--r--kernel/safe_typing.ml8
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/vconv.ml2
-rw-r--r--library/global.ml3
-rw-r--r--library/global.mli3
-rw-r--r--test-suite/coq-makefile/native1/_CoqProject1
-rw-r--r--tools/coqc.ml4
-rw-r--r--toplevel/coqargs.ml30
-rw-r--r--toplevel/coqargs.mli2
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--toplevel/usage.ml3
19 files changed, 76 insertions, 16 deletions
diff --git a/CHANGES.md b/CHANGES.md
index ada68f97d5..141e0c2333 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -24,6 +24,20 @@ Tactics
Simplex-based proof engine. In case of regression, 'Unset Simplex'
to get the venerable Fourier-based engine.
+Tools
+
+- The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
+ - `no` disables native_compute
+ - `yes` enables native_compute and precompiles `.v` files to native code
+ - `ondemand` enables native_compute but compiles code only when `native_compute` is called
+
+ The default value is `ondemand`.
+
+ Note that this flag now has priority over the configure flag of the same name.
+
+- A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls whether
+ conversion can use the VM. The default value is `yes`.
+
Changes from 8.8.2 to 8.9+beta1
===============================
diff --git a/checker/cic.mli b/checker/cic.mli
index 4162903b04..754cc2a096 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -221,6 +221,8 @@ type typing_flags = {
check_universes : bool; (** If [false] universe constraints are not checked *)
conv_oracle : oracle; (** Unfolding strategies for conversion *)
share_reduction : bool; (** Use by-need reduction algorithm *)
+ enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
+ enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
}
type constant_body = {
diff --git a/checker/values.ml b/checker/values.ml
index 24f10b7a87..8f6b24ec26 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 a127e0c2322c7846914bbca9921309c7 checker/cic.mli
+MD5 b8f0139f14e3370cd0a45d4cf69882ea checker/cic.mli
*)
@@ -230,7 +230,7 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|]
+ v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
diff --git a/configure.ml b/configure.ml
index f884a7de5c..39c65683ff 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1332,7 +1332,7 @@ let write_makefile f =
pr "# Option to control compilation and installation of the documentation\n";
pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no");
pr "# Option to produce precompiled files for native_compute\n";
- pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else "");
+ pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler yes" else "");
pr "COQWARNERROR=%s\n" (if !prefs.warn_error then "-w +default" else "");
close_out o;
Unix.chmod f 0o444
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 61fcb4832a..c1b38b4156 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -66,6 +66,8 @@ type typing_flags = {
check_universes : bool; (** If [false] universe constraints are not checked *)
conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
share_reduction : bool; (** Use by-need reduction algorithm *)
+ enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
+ enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
}
(* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d995786d97..3ed599c538 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -22,6 +22,8 @@ let safe_flags oracle = {
check_universes = true;
conv_oracle = oracle;
share_reduction = true;
+ enable_VM = true;
+ enable_native_compiler = true;
}
(** {6 Arities } *)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 054b6a2d17..f5d7ab3c9d 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -14,7 +14,8 @@ open Nativelib
open Reduction
open Util
open Nativevalues
-open Nativecode
+open Nativecode
+open Environ
(** This module implements the conversion test by compiling to OCaml code *)
@@ -142,7 +143,7 @@ let warn_no_native_compiler =
strbrk " falling back to VM conversion test.")
let native_conv_gen pb sigma env univs t1 t2 =
- if not Coq_config.native_compiler then begin
+ if not (typing_flags env).Declarations.enable_native_compiler then begin
warn_no_native_compiler ();
Vconv.vm_conv_gen pb env univs t1 t2
end
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index d294f2060e..833e4082f0 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -66,7 +66,6 @@ let warn_native_compiler_failed =
CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
let call_compiler ?profile:(profile=false) ml_filename =
- let () = assert Coq_config.native_compiler in
let load_path = !get_load_paths () in
let load_path = List.map (fun dn -> dn / output_dir) load_path in
let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (include_dirs () @ load_path)) in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 779e05ee0c..4b64cc6d11 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -198,6 +198,14 @@ let set_share_reduction b senv =
let flags = Environ.typing_flags senv.env in
set_typing_flags { flags with share_reduction = b } senv
+let set_VM b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with enable_VM = b } senv
+
+let set_native_compiler b senv =
+ let flags = Environ.typing_flags senv.env in
+ set_typing_flags { flags with enable_native_compiler = b } senv
+
(** Check that the engagement [c] expected by a library matches
the current (initial) one *)
let check_engagement env expected_impredicative_set =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 443b5cfd73..8fb33b04d4 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -138,6 +138,8 @@ val add_constraints :
val set_engagement : Declarations.engagement -> safe_transformer0
val set_typing_flags : Declarations.typing_flags -> safe_transformer0
val set_share_reduction : bool -> safe_transformer0
+val set_VM : bool -> safe_transformer0
+val set_native_compiler : bool -> safe_transformer0
(** {6 Interactive module functions } *)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 5965853e1e..c1130e62c9 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -189,7 +189,7 @@ let warn_bytecode_compiler_failed =
strbrk "falling back to standard conversion")
let vm_conv_gen cv_pb env univs t1 t2 =
- if not Coq_config.bytecode_compiler then
+ if not (typing_flags env).Declarations.enable_VM then
Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
full_transparent_state env univs t1 t2
else
diff --git a/library/global.ml b/library/global.ml
index bfea6d3dea..4ea5969a6f 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -186,3 +186,6 @@ let set_strategy k l =
let set_share_reduction b =
globalize0 (Safe_typing.set_share_reduction b)
+
+let set_VM b = globalize0 (Safe_typing.set_VM b)
+let set_native_compiler b = globalize0 (Safe_typing.set_native_compiler b)
diff --git a/library/global.mli b/library/global.mli
index 762a3f006d..01ee695c49 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -154,6 +154,9 @@ val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
val set_share_reduction : bool -> unit
+val set_VM : bool -> unit
+val set_native_compiler : bool -> unit
+
(* Modifies the global state, registering new universes *)
val current_modpath : unit -> ModPath.t
diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject
index 847b2c00a9..3dfca7ffc0 100644
--- a/test-suite/coq-makefile/native1/_CoqProject
+++ b/test-suite/coq-makefile/native1/_CoqProject
@@ -2,6 +2,7 @@
-R theories test
-I src
-arg -native-compiler
+-arg yes
src/test_plugin.mlpack
src/test.mlg
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 2cbf05bd8b..ad845470ec 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -97,7 +97,7 @@ let parse_args () =
|"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
|"-q"|"-profile"|"-echo" |"-quiet"
|"-silent"|"-m"|"-beautify"|"-strict-implicit"
- |"-impredicative-set"|"-vm"|"-native-compiler"
+ |"-impredicative-set"|"-vm"
|"-indices-matter"|"-quick"|"-type-in-type"
|"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
|"-stm-debug"
@@ -111,7 +111,7 @@ let parse_args () =
|"-load-ml-source"|"-require"|"-load-ml-object"
|"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
|"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
- |"-o"|"-profile-ltac-cutoff"|"-mangle-names"
+ |"-o"|"-profile-ltac-cutoff"|"-mangle-names"|"-bytecode-compiler"|"-native-compiler"
as o) :: rem ->
begin
match rem with
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 9918adfed3..8c643a285e 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -8,8 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-let warning s = Flags.(with_option warn Feedback.msg_warning (Pp.strbrk s))
-
let fatal_error exn =
Topfmt.print_err_exn Topfmt.ParsingCommandLine exn;
let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
@@ -66,6 +64,8 @@ type coq_cmdopts = {
color : color;
impredicative_set : Declarations.set_predicativity;
+ enable_VM : bool;
+ enable_native_compiler : bool;
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
diffs_set : bool;
@@ -116,6 +116,8 @@ let init_args = {
color = `AUTO;
impredicative_set = Declarations.PredicativeSet;
+ enable_VM = true;
+ enable_native_compiler = Coq_config.native_compiler;
stm_flags = Stm.AsyncOpts.default_opts;
debug = false;
diffs_set = false;
@@ -508,6 +510,26 @@ let parse_args arglist : coq_cmdopts * string list =
|"-o" -> { oval with compilation_output_name = Some (next()) }
+ |"-bytecode-compiler" ->
+ { oval with enable_VM = get_bool opt (next ()) }
+
+ |"-native-compiler" ->
+
+ (* We use two boolean flags because the four states make sense, even if
+ only three are accessible to the user at the moment. The selection of the
+ 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) =
+ match (next ()) with
+ | ("yes" | "on") -> true, true
+ | "ondemand" -> true, false
+ | ("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 }
+
(* Options with zero arg *)
|"-async-queries-always-delegate"
|"-async-proofs-always-delegate"
@@ -542,10 +564,6 @@ let parse_args arglist : coq_cmdopts * string list =
|"-m"|"--memory" -> { oval with memory_stat = true }
|"-noinit"|"-nois" -> { oval with load_init = false }
|"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true }
- |"-native-compiler" ->
- if not Coq_config.native_compiler then
- warning "Native compilation was disabled at configure time."
- else Flags.output_native_objects := true; oval
|"-output-context" -> { oval with output_context = true }
|"-profile-ltac" -> Flags.profile_ltac := true; oval
|"-q" -> { oval with load_rcfile = false; }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 7b0cdcf127..accb6c2beb 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -41,6 +41,8 @@ type coq_cmdopts = {
color : color;
impredicative_set : Declarations.set_predicativity;
+ enable_VM : bool;
+ enable_native_compiler : bool;
stm_flags : Stm.AsyncOpts.stm_opt;
debug : bool;
diffs_set : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8cd262c6d6..e4d9e9ac25 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -456,6 +456,8 @@ let init_toplevel custom_init arglist =
Flags.if_verbose print_header ();
Mltop.init_known_plugins ();
Global.set_engagement opts.impredicative_set;
+ Global.set_VM opts.enable_VM;
+ Global.set_native_compiler opts.enable_native_compiler;
(* Allow the user to load an arbitrary state here *)
inputstate opts;
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index d85fed5f43..c2437836f3 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -87,7 +87,8 @@ let print_usage_channel co command =
\n (use environment variable\
\n OCAML_GC_STATS=\"/tmp/gclog.txt\"\
\n for full Gc stats dump)\
-\n -native-compiler precompile files for the native_compute machinery\
+\n -bytecode-compiler (yes|no) controls the vm_compute machinery\
+\n -native-compiler (yes|no|ondemand) controls the native_compute machinery\
\n -h, -help, --help print this list of options\
\n";
List.iter (fun (name, text) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 12:30:26 +0000