Centralize the flag handling native compilation.

Instead of relying on the Coq_config immutable flag, we introduce an
initialization-only flag to govern the use of the native compiler. This
allows to make coqc passed with "-native-compiler no" behave as if it had
been configured without native compilation.

6 files changed, 21 insertions, 6 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index b87ba46634..1fe52c3b95 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 86a922847f..0e438e2358 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 2db674d397..f87a350728 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -486,8 +486,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 fc7b126ee5..7ed2e67e4c 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 46dd693155..87eafa251e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -233,6 +233,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 244424de6b..6ed38410c4 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -159,11 +159,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;