diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-14 09:53:36 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-05-14 09:53:36 +0200 |
| commit | 4ad6855504db2ce15a474bd646e19151aa8142e2 (patch) | |
| tree | b72697c8450705186f1337fe9cc9883106dc458d /kernel | |
| parent | d91addb140ba7315d70c4599b0d058bef798ac1c (diff) | |
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.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativeconv.ml | 5 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
2 files changed, 4 insertions, 5 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 75a3fc458..1f8bfc984 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -121,9 +121,8 @@ and conv_fix env lvl t1 f1 t2 f2 cu = aux 0 let native_conv pb sigma env t1 t2 = - if !Flags.no_native_compiler then begin - let msg = "Native compiler is disabled, "^ - "falling back to VM conversion test." in + if Coq_config.no_native_compiler then begin + let msg = "Native compiler is disabled, falling back to VM conversion test." in Pp.msg_warning (Pp.str msg); vm_conv pb env t1 t2 end diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d762a246e..d6bd75478 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -772,9 +772,9 @@ let export ?except senv dir = } in let ast, values = - if !Flags.no_native_compiler then [], [||] - else + if !Flags.native_compiler then Nativelibrary.dump_library mp dir senv.env str + else [], [||] in let lib = { comp_name = dir; |