diff options
| -rw-r--r-- | lib/flags.ml | 8 | ||||
| -rw-r--r-- | lib/flags.mli | 5 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 4 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | vernac/library.ml | 7 |
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; |