From 9dc9bd9468cd7bf72715dab4b0a074664667a3ad Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 17 Sep 2011 20:26:28 +0000 Subject: 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 --- Makefile.doc | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) (limited to 'Makefile.doc') 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 @@ -135,6 +141,14 @@ refman-quick: ../tools/show_latex_messages -no-overfull Reference-Manual.log && \ $(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@.*\(.*\).*, .*@\1,\2@' > $@ + + ###################################################################### # Tutorial ###################################################################### @@ -280,16 +294,6 @@ doc/RecTutorial/RecTutorial.pdf: doc/common/version.tex doc/common/title.tex doc 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@.*\(.*\).*, .*@\1,\2@' > doc/refman/html/index_urls.txt - - ###################################################################### # Install all documentation files ###################################################################### -- cgit v1.2.3