Merge PR #9525: Remove global output_native_objects flag.

Reviewed-by: ejgallego
Reviewed-by: maximedenes

4 files changed, 25 insertions, 12 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index ecb0407f75..8064ee8880 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -96,6 +96,9 @@ let compile opts copts ~echo ~f_in ~f_out =
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.stm_flags in
+  let output_native_objects = match opts.native_compiler with
+    | NativeOff -> false | NativeOn {ondemand} -> not ondemand
+  in
   match copts.compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
@@ -126,7 +129,7 @@ let compile opts copts ~echo ~f_in ~f_out =
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
+      Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
       Aux_file.record_in_aux_at "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
@@ -170,7 +173,7 @@ let compile opts copts ~echo ~f_in ~f_out =
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
       let doc = Stm.finish ~doc:state.doc in
       check_pending_proofs ();
-      let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
+      let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in
       Stm.reset_task_queue ()
 
   | Vio2Vo ->
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index ae3c5b32dc..b549f22119 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -33,6 +33,8 @@ let set_type_in_type () =
 
 type color = [`ON | `AUTO | `OFF]
 
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
 type t = {
 
   boot : bool;
@@ -56,7 +58,7 @@ type t = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter : bool;
   enable_VM : bool;
-  enable_native_compiler : bool;
+  native_compiler : native_compiler;
 
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
@@ -81,6 +83,11 @@ type t = {
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
 
+let default_native =
+  if Coq_config.native_compiler
+  then NativeOn {ondemand=true}
+  else NativeOff
+
 let default = {
 
   boot = false;
@@ -103,7 +110,8 @@ let default = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
   enable_VM = true;
-  enable_native_compiler = Coq_config.native_compiler;
+  native_compiler = default_native;
+
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
   diffs_set    = false;
@@ -418,15 +426,14 @@ let parse_args ~help ~init arglist : t * string list =
       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) =
+      let native_compiler =
         match (next ()) with
-        | ("yes" | "on") -> true, true
-        | "ondemand" -> true, false
-        | ("no" | "off") -> false, false
+        | ("yes" | "on") -> NativeOn {ondemand=false}
+        | "ondemand" -> NativeOn {ondemand=true}
+        | ("no" | "off") -> NativeOff
         | _ -> 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 }
+      { oval with native_compiler }
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 52ab2b60d7..9cc846edea 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -12,6 +12,8 @@ type color = [`ON | `AUTO | `OFF]
 
 val default_toplevel : Names.DirPath.t
 
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
 type t = {
 
   boot : bool;
@@ -34,7 +36,8 @@ type t = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter : bool;
   enable_VM : bool;
-  enable_native_compiler : bool;
+  native_compiler : native_compiler;
+
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
   diffs_set   : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index faf26a9665..c2c538edea 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -188,7 +188,7 @@ let init_toplevel ~help ~init custom_init arglist =
   Global.set_engagement opts.impredicative_set;
   Global.set_indices_matter opts.indices_matter;
   Global.set_VM opts.enable_VM;
-  Global.set_native_compiler opts.enable_native_compiler;
+  Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
 
   (* Allow the user to load an arbitrary state here *)
   inputstate opts;