From 4ad6855504db2ce15a474bd646e19151aa8142e2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 14 May 2015 09:53:36 +0200
Subject: 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.
---
 tools/coqc.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 7e822dbe36..31e0a0e0ad 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -109,7 +109,7 @@ let parse_args () =
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
-      |"-impredicative-set"|"-vm"|"-no-native-compiler"
+      |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-verbose-compat-notations"|"-no-compat-notations"
       |"-indices-matter"|"-quick"|"-color"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
-- 
cgit v1.2.3


From 81eb133d64ac81cbf6962d624b20c1aa55c2baae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 Apr 2015 11:16:05 +0200
Subject: Adding an option -w to control Coq warning output.

For now, warnings are still ignored by default, but this may change. This
commit at least allows to print them whenever desired. The -w syntax is
also opened to future additions to further control the display of
warnings.
---
 tools/coqc.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 31e0a0e0ad..aed229abc8 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -122,7 +122,7 @@ let parse_args () =
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
-      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
+      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"|"-w"
       as o) :: rem ->
 	begin
 	  match rem with
-- 
cgit v1.2.3


From 3fb81febe8efc34860688cac88a2267cfe298cf7 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 14 May 2015 16:38:21 +0200
Subject: Do not regenerate .d files when cleaning them. (Fix bug #4079)

---
 tools/coq_makefile.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 00088570b3..8f4772e286 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -575,8 +575,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
   let decl_var var = function
     |[] -> ()
     |l ->
-      printf "%s:=" var; print_list "\\\n  " l; print "\n";
-      printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var
+      printf "%s:=" var; print_list "\\\n  " l; print "\n\n";
+      print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n";
+      printf "-include $(addsuffix .d,$(%s))\n" var;
+      print "else\nifeq ($(MAKECMDGOALS),)\n";
+      printf "-include $(addsuffix .d,$(%s))\n" var;
+      print "endif\nendif\n\n";
+      printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var
   in
   section "Files dispatching.";
   decl_var "VFILES" vfiles;
-- 
cgit v1.2.3