Various fixes in the Makefiles

 After a successful build, re-doing make world should almost do nothing.
 For that:
  - Many targets added to .PHONY, especially "tools" since a "tools"
    directory exists. And anyway this is said to speed-up make a bit.
  - Concerning fake_ide, mentionning the .cm* instead of the .ml*
    avoid rebuilding these .cm*, and hence possibly many other things.
  - in Makefile.doc: fix the rule building index_url.txt
  - coqtop.* is now built by $(BESTCOQMKTOP) instead of $(COQMKTOP)
    (which is the symlink). This avoids a situation where a first
    "make" could redo just a few files while a second "make" will
    rebuild many more. Typical scenario : touch the Makefile,
    1st make was re-doing tolink.ml and then coqmktop, but no more,
    a 2nd make was then detecting that coqtop and the stdlib was to
    be redone

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

4 files changed, 52 insertions, 24 deletions

diff --git a/Makefile.build b/Makefile.build
index 925e537f5..857cb3914 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -187,6 +187,8 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
+.PHONY: coqbinaries coq coqlib coqlight states
+
 coqbinaries:: ${COQBINARIES} ${CSDPCERT} ${FAKEIDE}
 
 coq: coqlib tools coqbinaries
@@ -197,14 +199,14 @@ coqlight: theories-light tools coqbinaries
 
 states:: states/initial.coq
 
-$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
+$(COQTOPOPT): $(BESTCOQMKTOP) $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@
+	$(HIDE)$(BESTCOQMKTOP) -boot -opt $(OPTFLAGS) -o $@
 	$(STRIP) $@
 
-$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
+$(COQTOPBYTE): $(BESTCOQMKTOP) $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@
+	$(HIDE)$(BESTCOQMKTOP) -boot -top $(BYTEFLAGS) -o $@
 
 $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
 	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
@@ -292,6 +294,8 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
 # CoqIde special targets
 ###########################################################################
 
+.PHONY: coqide coqide-binaries coqide-no coqide-byte coqide-opt coqide-files
+
 # target to build CoqIde
 coqide:: coqide-files coqide-binaries states
 
@@ -323,6 +327,9 @@ $(COQIDE):
 
 # install targets
 
+.PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt
+.PHONY: install-ide-files install-ide-info install-im
+
 FULLIDELIB=$(FULLCOQLIB)/ide
 
 install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info
@@ -364,13 +371,14 @@ install-im:
 # tests
 ###########################################################################
 
+.PHONY: validate check test-suite $(ALLSTDLIB).v
+
 VALIDOPTS=-silent -o -m
 
 validate:: $(BESTCHICKEN) $(ALLVO)
 	$(SHOW)'COQCHK <theories & plugins>'
 	$(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
 
-.PHONY: $(ALLSTDLIB).v
 $(ALLSTDLIB).v:
 	$(SHOW)'MAKE $(notdir $@)'
 	$(HIDE)echo "Require $(ALLMODS)." > $@
@@ -388,6 +396,9 @@ test-suite: world $(ALLSTDLIB).v
 # partial targets: 1) core ML parts
 ##################################################################
 
+.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
+.PHONY: highparsing toplevel hightactics
+
 lib: lib/lib.cma
 kernel: kernel/kernel.cma
 byterun: $(BYTERUN)
@@ -405,6 +416,10 @@ hightactics: tactics/hightactics.cma
 # 2) theories and plugins files
 ###########################################################################
 
+.PHONY: init theories theories-light
+.PHONY: logic arith bool narith zarith qarith lists strings sets
+.PHONY: fsets relations wellfounded reals setoids sorting numbers noreal
+
 init: $(INITVO)
 
 theories: $(THEORIESVO)
@@ -434,6 +449,9 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 # 3) plugins
 ###########################################################################
 
+.PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction
+.PHONY: field fourier funind cc subtac rtauto pluginsopt
+
 plugins: $(PLUGINSVO)
 omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
 micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
@@ -472,6 +490,8 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g
 # tools
 ###########################################################################
 
+.PHONY: printers tools
+
 printers: $(DEBUGPRINTERS)
 
 tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
@@ -511,7 +531,7 @@ $(COQDOC): $(COQDOCCMO:.cmo=$(BESTOBJ))
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-$(FAKEIDE): toplevel/ide_intf.mli toplevel/ide_intf.ml tools/fake_ide.ml
+$(FAKEIDE): toplevel/ide_intf$(BESTOBJ) tools/fake_ide$(BESTOBJ)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,unix)
 
@@ -556,6 +576,10 @@ FULLCOQDOCDIR=$(COQDOCDIR)
 FULLDOCDIR=$(DOCDIR)
 endif
 
+.PHONY: install-coq install-coqlight install-binaries install-byte install-opt
+.PHONY: install-tools install-library install-library-light
+.PHONY: install-coq-info install-coq-manpages install-emacs install-latex
+
 install-coq: install-binaries install-library install-coq-info
 install-coqlight: install-binaries install-library-light
 
diff --git a/Makefile.common b/Makefile.common
index cd8f2063b..b7ff5da4f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -16,18 +16,22 @@ COQMKTOPBYTE:=bin/coqmktop.byte$(EXE)
 COQMKTOPOPT:=bin/coqmktop.opt$(EXE)
 BESTCOQMKTOP:=bin/coqmktop.$(BEST)$(EXE)
 COQMKTOP:=bin/coqmktop$(EXE) 
+
 COQCBYTE:=bin/coqc.byte$(EXE)
 COQCOPT:=bin/coqc.opt$(EXE)
 BESTCOQC:=bin/coqc.$(BEST)$(EXE)
 COQC:=bin/coqc$(EXE)
+
 COQTOPBYTE:=bin/coqtop.byte$(EXE)
 COQTOPOPT:=bin/coqtop.opt$(EXE)
 BESTCOQTOP:=bin/coqtop.$(BEST)$(EXE)
 COQTOPEXE:=bin/coqtop$(EXE)
+
 CHICKENBYTE:=bin/coqchk.byte$(EXE)
 CHICKENOPT:=bin/coqchk.opt$(EXE)
 BESTCHICKEN:=bin/coqchk.$(BEST)$(EXE)
 CHICKEN:=bin/coqchk$(EXE)
+
 FAKEIDE:=bin/fake_ide$(EXE)
 
 ifeq ($(CAMLP4),camlp4)
@@ -66,7 +70,6 @@ BESTOBJ:=$(if $(OPT),.cmx,.cmo)
 COQBINARIES:= $(COQMKTOP) $(COQC) \
   $(COQTOPBYTE) $(if $(OPT),$(COQTOPOPT)) $(COQTOPEXE) \
   $(CHICKENBYTE) $(if $(OPT),$(CHICKENOPT)) $(CHICKEN)
-OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
 
 CSDPCERT:=plugins/micromega/csdpcert$(EXE)
 
diff --git a/Makefile.doc b/Makefile.doc
index dc3ae8b5f..42f9bf7aa 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -11,9 +11,12 @@
 ### General rules
 ######################################################################
 
-.PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial
+.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial
+.PHONY: stdlib full-stdlib faq rectutorial
 
-doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt
+INDEXURLS:=doc/refman/html/index_url.txt
+
+doc: refman faq tutorial rectutorial stdlib $(INDEXURLS)
 
 doc-html:\
   doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
@@ -120,8 +123,11 @@ doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html
 doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva
 	$(INSTALLLIB) $< doc/refman
 
-doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
-                        doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
+INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html
+ALLINDEXES:= doc/refman/html/index.html $(INDEXES)
+
+$(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
+	       doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
 	- rm -rf doc/refman/html
 	$(MKDIR) doc/refman/html
 	$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
@@ -136,6 +142,14 @@ refman-quick:
 	$(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)
 
 ######################################################################
+# Index file for CoqIDE
+######################################################################
+
+doc/refman/html/index_url.txt: $(INDEXES)
+	cat $< | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > $@
+
+
+######################################################################
 # Tutorial
 ######################################################################
 
@@ -281,16 +295,6 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
 	(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)
 
 ######################################################################
-# Index file for CoqIDE
-######################################################################
-
-# Not robust, improve...
-ide/index_urls.txt: doc/refman/html/index.html
-	@ rm -f doc/refman/html/index_urls.txt
-	cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > doc/refman/html/index_urls.txt
-
-
-######################################################################
 # Install all documentation files
 ######################################################################
 
diff --git a/test-suite/Makefile b/test-suite/Makefile
index e628614ab..828a710b1 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -97,9 +97,6 @@ clean:
 	  -name '*.stamp' -o -name '*.vo' -o -name '*.log' \
 	\) -print0 | xargs -0 rm -f
 
-distclean: clean
-	$(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f
-
 #######################################################################
 # Per-subsystem targets
 #######################################################################