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

4 files changed, 30 insertions, 7 deletions

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