From 26911bbc0bb3347c922d12b07a1c2bc34bba3c8d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 9 Jul 2015 13:55:36 +0200
Subject: Improve semantics of -native-compiler flag.

Since Guillaume's, launching coqtop without -native-compiler and call
native_compute would mean recompiling silently all dependencies, even if they
had been precompiled (e.g. the stdlib).

The new semantics is that -native-compiler disables separate compilation of the
current library, but still tries to load precompiled dependencies. If loading
fails when the flag is on, coqtop stays silent.
---
 kernel/nativelib.ml | 8 +++++---
 library/library.ml  | 5 +++--
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 7cb01b6955..70920f1bbe 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -110,9 +110,11 @@ let call_linker ?(fatal=true) prefix f upds =
   rt1 := dummy_value ();
   rt2 := dummy_value ();
   if not (Sys.file_exists f) then
-    let msg = "Cannot find native compiler file " ^ f in
-    if fatal then Errors.error msg
-    else Pp.msg_warning (Pp.str msg)
+    begin
+      let msg = "Cannot find native compiler file " ^ f in
+      if fatal then Errors.error msg
+      else if !Flags.native_compiler then Pp.msg_warning (Pp.str msg)
+    end
   else
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
diff --git a/library/library.ml b/library/library.ml
index a8fbe0841c..45fce1c26c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -169,8 +169,9 @@ 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 !Flags.native_compiler then
-      Nativelib.link_library ~prefix ~dirname ~basename:f
+    (* This will not produce errors or warnings if the native compiler was
+       not enabled *)
+    Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [libname]
-- 
cgit v1.2.3