Coq_makefile does not install/compile explicitely cmo and cmxs? that are in a cmx?a

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14598 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 18 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index d3e92489b5..4a60cc8ea2 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -245,7 +245,8 @@ let clean sds sps =
   print "clean:\n";
   print "\trm -f *~ Makefile-localvars.gen\n";
   if !some_mlfile || !some_mlifile || !some_ml4file || !some_mllibfile then begin
-    print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMAFILES) $(CMXAFILES) $(CMXSFILES) $(OFILES)\n";
+    print "\trm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)\n";
+    print "\trm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)\n";
     print "\trm -f $(MLFILES:.ml=.ml.d) $(MLIFILES:.mli=.mli.d) $(ML4FILES:.ml4=.ml4.d) $(MLLIBFILES:.mllib=.mllib.d)\n";
   end;
   if !some_vfile then
@@ -272,13 +273,6 @@ let clean sds sps =
 
 let header_includes () = ()
 
-let footer_includes () =
-  if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
-  if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n";
-  if !some_mlifile then print "-include $(MLIFILES:.mli=.mli.d)\n.SECONDARY: $(MLIFILES:.mli=.mli.d)\n\n";
-  if !some_ml4file then print "-include $(ML4FILES:.ml4=.ml4.d)\n.SECONDARY: $(ML4FILES:.ml4=.ml4.d)\n\n";
-  if !some_mllibfile then print "-include $(MLLIBFILES:.mllib=.mllib.d)\n.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)\n\n"
-
 let implicit () =
   let mli_rules () =
     print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
@@ -410,6 +404,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc
     |[] -> ()
     |l ->
       print "VFILES:="; print_list "\\\n  " l; print "\n";
+      print "\n-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
       print "VOFILES:=$(VFILES:.v=.vo)\n";
       classify_files_by_root "VOFILES" l inc;
       print "GLOBFILES:=$(VFILES:.v=.glob)\n";
@@ -422,28 +417,34 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc
     |[],[] -> []
     |[],ml ->
       print "MLFILES:="; print_list "\\\n  " ml; print "\n";
-      print "CMOFILES:=$(MLFILES:.ml=.cmo)\n";
+      print "\n-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n";
+      print "ALLCMOFILES:=$(MLFILES:.ml=.cmo)\n";
       ml
     |ml4,[] ->
       print "ML4FILES:="; print_list "\\\n  " ml4; print "\n";
-      print "CMOFILES:=$(ML4FILES:.ml4=.cmo)\n";
+      print "\n-include $(ML4FILES:.ml4=.ml4.d)\n.SECONDARY: $(ML4FILES:.ml4=.ml4.d)\n\n";
+      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo)\n";
       ml4
     |ml4,ml ->
       print "ML4FILES:="; print_list "\\\n  " ml4; print "\n";
+      print "\n-include $(ML4FILES:.ml4=.ml4.d)\n.SECONDARY: $(ML4FILES:.ml4=.ml4.d)\n\n";
       print "MLFILES:="; print_list "\\\n  " ml; print "\n";
-      print "CMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n";
+      print "\n-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n";
+      print "ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)\n";
       ml@ml4 in
+  print "CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))\n";
   begin match mlsfiles with
     |[] -> ()
     |l ->
       classify_files_by_root "CMOFILES" l inc;
-      print "CMXFILES:=$(CMOFILES:.cmo=.cmx)\n";
-      print "OFILES:=$(CMXFILES:.cmx=.o)\n";
+      print "CMXFILES=$(CMOFILES:.cmo=.cmx)\n";
+      print "OFILES=$(CMXFILES:.cmx=.o)\n";
   end;
   begin match mllibfiles with
     |[] -> ()
     |l ->
       print "MLLIBFILES:="; print_list "\\\n  " l; print "\n";
+      print "\n-include $(MLLIBFILES:.mllib=.mllib.d)\n.SECONDARY: $(MLLIBFILES:.mllib=.mllib.d)\n\n";
       print "CMAFILES:=$(MLLIBFILES:.mllib=.cma)\n";
       print "CMXAFILES:=$(CMAFILES:.cma=.cmxa)\n";
   end;
@@ -451,6 +452,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc
     |[] -> ()
     |l ->
       print "MLIFILES:="; print_list "\\\n  " l; print "\n";
+      print "\n-include $(MLIFILES:.mli=.mli.d)\n.SECONDARY: $(MLIFILES:.mli=.mli.d)\n\n";
   end;
   begin match mlifiles,mlfiles with
     |[],[] -> ()
@@ -458,10 +460,10 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc
        print "CMIFILES:=$(MLIFILES:.mli=.cmi)\n";
 	classify_files_by_root "CMIFILES" l inc;
     |[],l ->
-      print "CMIFILES:=$(CMOFILES:.cmo=.cmi)\n";
+      print "CMIFILES=$(ALLCMOFILES:.cmo=.cmi)\n";
       classify_files_by_root "CMIFILES" l inc;
     |l1,l2 ->
-      print "CMIFILES:=$(sort $(CMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n";
+      print "CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))\n";
       classify_files_by_root "CMIFILES" (l1@l2) inc;
   end;
   begin match mllibfiles,mlsfiles with
@@ -470,10 +472,10 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc
       print "CMXSFILES:=$(CMXAFILES:.cmxa=.cmxs)\n";
       classify_files_by_root "CMXSFILES" l inc;
     |[],l ->
-      print "CMXSFILES:=$(CMXFILES:.cmx=.cmxs)\n";
+      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs)\n";
       classify_files_by_root "CMXSFILES" l inc;
     |l1,l2 ->
-      print "CMXSFILES:=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n";
+      print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n";
       classify_files_by_root "CMXSFILES" (l1@l2) inc;
   end;
   print "\nall: ";
@@ -617,7 +619,6 @@ let do_makefile args =
   if is_install then install targets inc;
   clean sds sps;
   make_makefile sds;
-  footer_includes ();
   warning ();
   if not (makefile = None) then close_out !output_channel;
   exit 0