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 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'kernel')

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;
-- 
cgit v1.2.3