Merge PR #11306: Centralize the flag handling native compilation.

Ack-by: SkySkimmer
Reviewed-by: maximedenes

6 files changed, 21 insertions, 6 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 2832ddd27a..1d9d6d49bc 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -82,3 +82,11 @@ let get_inline_level () = !inline_level
 
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
+
+let native_compiler = ref None
+let get_native_compiler () = match !native_compiler with
+| None -> assert false
+| Some b -> b
+let set_native_compiler b =
+  let () = assert (!native_compiler == None) in
+  native_compiler := Some b
diff --git a/lib/flags.mli b/lib/flags.mli
index a68be196d7..30d1b5b2bd 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -90,6 +90,11 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 (** Temporarily extends the reference to a list *)
 val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
 
+(** Native compilation flag *)
+val get_native_compiler : unit -> bool
+val set_native_compiler : bool -> unit
+(** Must be set exactly once at initialization time. *)
+
 (** Level of inlining during a functor application *)
 val set_inline_level : int -> unit
 val get_inline_level : unit -> int
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 7be34d4cf1..f989dae4c9 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -496,8 +496,8 @@ let stop_profiler m_pid =
 let native_norm env sigma c ty =
   let c = EConstr.Unsafe.to_constr c in
   let ty = EConstr.Unsafe.to_constr ty in
-  if not Coq_config.native_compiler then
-    user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
+  if not (Flags.get_native_compiler ()) then
+    user_err Pp.(str "Native_compute reduction has been disabled.")
   else
   (*
   Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index 250c80d9a5..db09a2e69e 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -37,7 +37,7 @@ let warn_native_compute_disabled =
    strbrk "native_compute disabled at configure time; falling back to vm_compute.")
 
 let cbv_native env sigma c =
-  if Coq_config.native_compiler then
+  if Flags.get_native_compiler () then
     let ctyp = Retyping.get_type_of env sigma c in
     Nativenorm.native_norm env sigma c ctyp
   else
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a63cff3e6f..7d08244d49 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -197,6 +197,7 @@ let init_execution opts custom_init =
   Global.set_engagement opts.config.logic.impredicative_set;
   Global.set_indices_matter opts.config.logic.indices_matter;
   Global.set_VM opts.config.enable_VM;
+  Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
   Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
   Global.set_allow_sprop opts.config.logic.allow_sprop;
   if opts.config.logic.cumulative_sprop then Global.make_sprop_cumulative ();
diff --git a/vernac/library.ml b/vernac/library.ml
index 7c629b08e7..1b0bd4c0f7 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -155,11 +155,12 @@ let register_loaded_library m =
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
-    if Coq_config.native_compiler then
-      Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
+    Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
   in
   let rec aux = function
-    | [] -> link (); [libname]
+    | [] ->
+      let () = if Flags.get_native_compiler () then link () in
+      [libname]
     | m'::_ as l when DirPath.equal m' libname -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;