summaryrefslogtreecommitdiff
path: root/dev/tools/Makefile.dir
diff options
context:
space:
mode:
Diffstat (limited to 'dev/tools/Makefile.dir')
-rw-r--r--dev/tools/Makefile.dir131
1 files changed, 131 insertions, 0 deletions
diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir
new file mode 100644
index 00000000..68c917ac
--- /dev/null
+++ b/dev/tools/Makefile.dir
@@ -0,0 +1,131 @@
+# make a link to this file if you are working hard in one directory of Coq
+# ln -s ../dev/Makefile.dir Makefile
+# if you are working in a sub/dir/ make a link to dev/Makefile.subdir instead
+# this Makefile provides many useful facilities to develop Coq
+# it is not completely compatible with .ml4 files unfortunately
+
+ifndef TOPDIR
+TOPDIR=..
+endif
+
+# this complicated thing should work for subsubdirs as well
+BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||"))
+
+noargs: dir
+
+test-dir:
+ @echo TOPDIR=$(TOPDIR)
+ @echo BASEDIR=$(BASEDIR)
+
+include $(TOPDIR)/dev/tools/Makefile.common
+
+# make this directory
+dir:
+ $(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR))
+
+# make all cmo's in this directory. Useful in case the main Makefile is not
+# up-to-date
+all:
+ @( ( for i in *.ml; do \
+ echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \
+ done; \
+ for i in *.ml4; do \
+ echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \
+ done ) \
+ | xargs $(MAKE) -C $(TOPDIR) )
+
+# lists all files that should be compiled in this directory
+list:
+ @(for i in *.mli; do \
+ ls -l `basename $$i .mli`.cmi; \
+ done)
+ @(for i in *.ml; do \
+ ls -l `basename $$i .ml`.cmo; \
+ done)
+ @(for i in *.ml4; do \
+ ls -l `basename $$i .ml4`.cmo; \
+ done)
+
+
+clean::
+ rm -f *.cmi *.cmo *.cmx *.o
+
+
+# if grammar.cmo files cannot be compiled and main .depend cannot be
+# rebuilt, this is quite useful
+depend:
+ (cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
+
+
+# displays the dependency graph of the current directory (vertically,
+# unlike in doc/)
+graph:
+ (ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) &
+
+
+# the pretty entry draws a dependency graph marking red those nodes
+# which do not have their .cmo files
+
+.INTERMEDIATE: depend.dot depend.2.dot
+.PHONY: depend.ps
+
+depend.dot:
+ ocamldep *.ml *.mli | ocamldot > $@
+
+depend.2.dot: depend.dot
+ (i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@
+ (for ml in *.ml; do \
+ base=`basename $$ml .ml`; \
+ fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \
+ rest=`echo $$base | cut -c2-`; \
+ name=`echo $$fst $$rest | tr -d " "`; \
+ cmo=$$base.cmo; \
+ if [ ! -e $$cmo ]; then \
+ echo \"$$name\" [color=red]\; >> $@;\
+ fi;\
+ done;\
+ echo } >> $@)
+
+depend.ps: depend.2.dot
+ dot -Tps $< > $@
+
+clean::
+ rm -f depend.ps
+
+pretty: depend.ps
+ (gv -spartan $<; rm $<) &
+# gv -spartan $< &
+
+
+
+# generating file.ml.mli by tricking make to pass -i to ocamlc
+
+%.ml.mli: FORCE
+ @(cmo=`basename $@ .ml.mli`.cmo ; \
+ mv -f $$cmo $$cmo.tmp ; \
+ $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \
+ echo Generated interface file $@ ; \
+ mv -f $$cmo.tmp $$cmo)
+
+%.annot: FORCE
+ @(cmo=`basename $@ .annot`.cmo ; \
+ mv -f $$cmo $$cmo.tmp ; \
+ $(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \
+ echo Generated annotation file $@ ; \
+ mv -f $$cmo.tmp $$cmo)
+
+FORCE:
+
+clean::
+ rm -f *.ml.mli
+
+# this is not perfect but mostly WORKS! It just calls the main makefile
+
+%.cmi: FORCE
+ $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+%.cmo: FORCE
+ $(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+coqtop:
+ $(MAKE) -C $(TOPDIR) bin/coqtop.byte