diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.ml | 2 | ||||
| -rw-r--r-- | kernel/declareops.ml | 2 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 5 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 8 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | kernel/vconv.ml | 2 |
7 files changed, 18 insertions, 4 deletions
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 |