Amélioration de la génération des graphes de dépendances

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

4 files changed, 67 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index dabe3078c..4dfc5062d 100644
--- a/Makefile
+++ b/Makefile
@@ -107,7 +107,7 @@ else
 stage1 $(STAGE1_TARGETS): always
 	$(call stage-template,1)
 
-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa
+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.dep.ps %.dot
 ifdef CM_STAGE1
 $(CAML_OBJECT_PATTERNS): always
 	$(call stage-template,1)
@@ -134,9 +134,9 @@ endif #GOTO_STAGE
 # Cleaning
 ###########################################################################
 
-.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide ml4depclean depclean distclean cleanconfig cleantheories docclean
+.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide ml4depclean depclean distclean cleanconfig cleantheories docclean devdocclean
 
-clean: objclean cruftclean depclean docclean
+clean: objclean cruftclean depclean docclean devdocclean
 
 objclean: archclean indepclean
 
@@ -194,6 +194,9 @@ cleantheories:
 	rm -f states/*.coq
 	find theories -name '*.vo' -or -name '*.glob' | xargs rm -f
 
+devdocclean:
+	find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \;
+
 ###########################################################################
 # Emacs tags
 ###########################################################################
diff --git a/Makefile.build b/Makefile.build
index 0674e5bba..b6ce142a0 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -882,6 +882,44 @@ devel: $(DEBUGPRINTERS)
 
 ###########################################################################
 
+
+%.dot: %.mli
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< 
+
+%.types.dot: %.mli
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 
+
+%.dep.ps: %.dot
+	$(DOT) $(DOTOPTS) -o $@ $<
+
+kernel/kernel.dot: $(KERNELMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(KERNELMLI)
+
+interp/interp.dot: $(INTERPMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(INTERPMLI)
+
+pretyping/pretyping.dot: $(PRETYPINGMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(PRETYPINGMLI)
+
+library/library.dot: $(LIBRARYMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(LIBRARYMLI)
+
+parsing/parsing.dot: $(PARSINGMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(PARSINGMLI)
+
+tactics/tactics.dot: $(TACTICSMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(TACTICSMLI)
+
+proofs/proofs.dot: $(PROOFSMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(PROOFSMLI)
+
+toplevel/toplevel.dot: $(TOPLEVELMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(TOPLEVELMLI)
+
+coq.dot: $(COQMLI:.mli=.cmi)
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $(COQMLI)
+
+
 # For emacs: 
 # Local Variables: 
 # mode: makefile 
diff --git a/Makefile.common b/Makefile.common
index 919e9243e..69a2931ed 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -793,6 +793,24 @@ PCOQMANPAGES:=man/coq-interface.1 man/parser.1
 RECTYPESML:=kernel/term.ml library/nametab.ml proofs/tacexpr.ml \
   parsing/pptactic.ml 
 
+
+#########################################################
+# .mli files by directory (used for dependencies graphs #
+#########################################################
+
+# We use wildcard to get rid of .cmo that do not have a .mli 
+KERNELMLI:=$(wildcard $(KERNEL:.cmo=.mli))
+INTERPMLI:=$(wildcard $(INTERP:.cmo=.mli))
+PRETYPINGMLI:=$(wildcard $(PRETYPING:.cmo=.mli))
+TOPLEVELMLI:=$(wildcard $(TOPLEVEL:.cmo=.mli))
+PROOFSMLI:=$(wildcard $(PROOFS:.cmo=.mli))
+LIBRARYMLI:=$(wildcard $(LIBRARY:.cmo=.mli))
+PARSINGMLI:=$(wildcard $(PARSING:.cmo=.mli) $(HIGHPARSING:.cmo=.mli))
+TACTICSMLI:=$(wildcard $(TACTICS:.cmo=.mli) $(HIGHTACTICS:.cmo=.mli))
+COQMLI:=$(KERNELMLI) $(INTERPMLI) $(PRETYPINGMLI) $(TOPLEVELMLI) $(PROOFSMLI) \
+	$(LIBRARYMLI) $(PARSINGMLI) $(TACTICSMLI)
+
+
 ###########################################################################
 # Miscellaneous
 ###########################################################################
diff --git a/config/Makefile.template b/config/Makefile.template
index 16dc75894..67c4c34d1 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -133,6 +133,11 @@ HASCOQIDE=COQIDEOPT
 # Defining REVISION
 CHECKEDOUT=CHECKEDOUTSOURCETREE
 
+# Defining options to generate dependencies graphs
+DOT=dot
+DOTOPTS=-Tps
+ODOCDOTOPTS=-dot -dot-reduce
+
 # make or sed are bogus and believe lines not terminating by a return
 # are inexistent