Pass native and VM flags to the kernel through environment

The kernel no longer has to read the configure flag, its value can now
be overriden by a coqtop/coqc argument, and more generally is easier to
set from a toplevel (such as the checker).

We also add a `-bytecode-compiler` flag.

Fixes #4607

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) ->