From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 14 May 2015 09:53:36 +0200 Subject: Disable precompilation for native_compute by default. Note that this does not prevent using native_compute, but it will force on-the-fly recompilation of dependencies whenever it is used. Precompilation is enabled for the standard library, assuming native compilation was enabled at configuration time. If native compilation was disabled at configuration time, native_compute falls back to vm_compute. Failure to precompile is a hard error, since it is now explicitly required by the user. --- proofs/redexpr.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'proofs/redexpr.ml') diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d25f7e915..f172bbdd1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -30,9 +30,13 @@ let cbv_vm env sigma c = Vnorm.cbv_vm env c ctyp let cbv_native env sigma c = - let ctyp = Retyping.get_type_of env sigma c in - let evars = Nativenorm.evars_of_evar_map sigma in - Nativenorm.native_norm env evars c ctyp + if Coq_config.no_native_compiler then + let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in + cbv_vm env sigma c + else + let ctyp = Retyping.get_type_of env sigma c in + let evars = Nativenorm.evars_of_evar_map sigma in + Nativenorm.native_norm env evars c ctyp let whd_cbn flags env sigma t = let (state,_) = -- cgit v1.2.3