aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-05-14 09:53:36 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-05-14 09:53:36 +0200
commit4ad6855504db2ce15a474bd646e19151aa8142e2 (patch)
treeb72697c8450705186f1337fe9cc9883106dc458d /library/library.ml
parentd91addb140ba7315d70c4599b0d058bef798ac1c (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 'library/library.ml')
-rw-r--r--library/library.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/library/library.ml b/library/library.ml
index 1ffa1a305..0296d7b90 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -166,7 +166,7 @@ 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 not !Flags.no_native_compiler then
+ if !Flags.native_compiler then
Nativelib.link_library ~prefix ~dirname ~basename:f
in
let rec aux = function
@@ -788,10 +788,10 @@ let save_library_to ?todo dir f otab =
System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
(* Writing native code files *)
- if not !Flags.no_native_compiler then
+ if !Flags.native_compiler then
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Nativelib.compile_library dir ast fn) then
- msg_error (str"Could not compile the library to native code. Skipping.")
+ error "Could not compile the library to native code."
with reraise ->
let reraise = Errors.push reraise in
let () = msg_warning (str "Removed file " ++ str f') in