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/nativelib.ml') diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 7cb01b695..70920f1bb 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 From 8c7fa14c87dff113222469d138fee054b6c1ccb5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 10 Jul 2015 00:00:30 +0200 Subject: Native compiler: make non-fatal linking errors silent except in debug mode. --- kernel/nativelib.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/nativelib.ml') diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 70920f1bb..b2142b43c 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -113,7 +113,7 @@ let call_linker ?(fatal=true) prefix f upds = 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) + else if !Flags.debug then Pp.msg_debug (Pp.str msg) end else (try @@ -123,7 +123,7 @@ let call_linker ?(fatal=true) prefix f upds = let exn = Errors.push exn in let msg = "Dynlink error, " ^ Dynlink.error_message e in if fatal then (Pp.msg_error (Pp.str msg); iraise exn) - else Pp.msg_warning (Pp.str msg)); + else if !Flags.debug then Pp.msg_debug (Pp.str msg)); match upds with Some upds -> update_locations upds | _ -> () let link_library ~prefix ~dirname ~basename = -- cgit v1.2.3