Merge PR #8870: Pass native and VM flags to the kernel through environment

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