Merge PR #9525: Remove global output_native_objects flag.

Reviewed-by: ejgallego
Reviewed-by: maximedenes

16 files changed, 44 insertions, 33 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 474ce3e871..18a257047d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1114,7 +1114,7 @@ let start_library dir senv =
     modvariant = LIBRARY;
     required = senv.required }
 
-let export ?except senv dir =
+let export ?except ~output_native_objects senv dir =
   let senv =
     try join_safe_environment ?except senv
     with e ->
@@ -1136,7 +1136,7 @@ let export ?except senv dir =
     }
   in
   let ast, symbols =
-    if !Flags.output_native_objects then
+    if output_native_objects then
       Nativelibrary.dump_library mp dir senv.env str
     else [], Nativecode.empty_symbols
   in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1b7239da23..8539fdd504 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -187,7 +187,7 @@ val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.sym
 val start_library : DirPath.t -> ModPath.t safe_transformer
 
 val export :
-  ?except:Future.UUIDSet.t ->
+  ?except:Future.UUIDSet.t -> output_native_objects:bool ->
   safe_environment -> DirPath.t ->
     ModPath.t * compiled_library * native_library
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 9e0d7ed380..768d359cce 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -116,8 +116,5 @@ let inline_level = ref default_inline_level
 let set_inline_level = (:=) inline_level
 let get_inline_level () = !inline_level
 
-(* Native code compilation for conversion and normalization *)
-let output_native_objects = ref false
-
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
diff --git a/lib/flags.mli b/lib/flags.mli
index 1066f31a8b..4ef5fb4445 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -110,9 +110,6 @@ val set_inline_level : int -> unit
 val get_inline_level : unit -> int
 val default_inline_level : int
 
-(** When producing vo objects, also compile the native-code version *)
-val output_native_objects : bool ref
-
 (** Global profile_ltac flag  *)
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 8699583cdf..5fd11e187a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -928,10 +928,10 @@ let append_end_library_hook f =
   let old_f = !end_library_hook in
   end_library_hook := fun () -> old_f(); f ()
 
-let end_library ?except dir =
+let end_library ?except ~output_native_objects dir =
   !end_library_hook();
   let oname = Lib.end_compilation_checks dir in
-  let mp,cenv,ast = Global.export ?except dir in
+  let mp,cenv,ast = Global.export ?except ~output_native_objects dir in
   let prefix, lib_stack = Lib.end_compilation oname in
   assert (ModPath.equal mp (MPfile dir));
   let substitute, keep, _ = Lib.classify_segment lib_stack in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 7aa4bc30ce..2b28ba908e 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -99,7 +99,7 @@ val get_library_native_symbols : library_name -> Nativecode.symbols
 val start_library : library_name -> unit
 
 val end_library :
-  ?except:Future.UUIDSet.t -> library_name ->
+  ?except:Future.UUIDSet.t -> output_native_objects:bool -> library_name ->
     Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
 (** append a function to be executed at end_library *)
diff --git a/library/global.ml b/library/global.ml
index 784a02449c..cf996ce644 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -143,7 +143,8 @@ let mind_of_delta_kn kn =
 (** Operations on libraries *)
 
 let start_library dir = globalize (Safe_typing.start_library dir)
-let export ?except s = Safe_typing.export ?except (safe_env ()) s
+let export ?except ~output_native_objects s =
+  Safe_typing.export ?except ~output_native_objects (safe_env ()) s
 let import c u d = globalize (Safe_typing.import c u d)
 
 
diff --git a/library/global.mli b/library/global.mli
index df18625a5f..4e2ad92717 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -108,7 +108,7 @@ val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.
 (** {6 Compiled libraries } *)
 
 val start_library : DirPath.t -> ModPath.t
-val export : ?except:Future.UUIDSet.t -> DirPath.t ->
+val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> DirPath.t ->
   ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest ->
diff --git a/library/library.ml b/library/library.ml
index 9b9bd07c93..37dadadb76 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -657,7 +657,7 @@ let error_recursively_dependent_library dir =
 (* Security weakness: file might have been changed on disk between
    writing the content and computing the checksum... *)
 
-let save_library_to ?todo dir f otab =
+let save_library_to ?todo ~output_native_objects dir f otab =
   let except = match todo with
     | None ->
         (* XXX *)
@@ -668,7 +668,7 @@ let save_library_to ?todo dir f otab =
         assert(Filename.check_suffix f ".vio");
         List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
           Future.UUIDSet.empty l in
-  let cenv, seg, ast = Declaremods.end_library ~except dir in
+  let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
   let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
   let tasks, utab, dtab =
     match todo with
@@ -716,7 +716,7 @@ let save_library_to ?todo dir f otab =
     System.marshal_out_segment f' ch (opaque_table : seg_proofs);
     close_out ch;
     (* Writing native code files *)
-    if !Flags.output_native_objects then
+    if output_native_objects then
       let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
       if not (Nativelib.compile_library dir ast fn) then
 	user_err Pp.(str "Could not compile the library to native code.")
diff --git a/library/library.mli b/library/library.mli
index c016352808..a976be0184 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -38,9 +38,11 @@ type seg_proofs = Constr.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid list -> unit
 
-(** End the compilation of a library and save it to a ".vo" file *)
+(** End the compilation of a library and save it to a ".vo" file.
+    [output_native_objects]: when producing vo objects, also compile the native-code version. *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
+  output_native_objects:bool ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit
 
 val load_library_todo :
diff --git a/stm/stm.ml b/stm/stm.ml
index e7833f253e..b4f26570c6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2890,11 +2890,12 @@ let handle_failure (e, info) vcs =
   VCS.print ();
   Exninfo.iraise (e, info)
 
-let snapshot_vio ~doc ldir long_f_dot_vo =
+let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo =
   let doc = finish ~doc in
   if List.length (VCS.branches ()) > 1 then
     CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
-  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
+  Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects
+    ldir long_f_dot_vo
     (Global.opaque_tables ());
   doc
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 313ac58111..102e832d3e 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -160,7 +160,7 @@ val join : doc:doc -> doc
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
      of the completed tasks is a failure) *)
-val snapshot_vio : doc:doc -> DirPath.t -> string -> doc
+val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
  * after having built a .vio in batch mode *)
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;