blob: 1a1bb90b44c056c9e8714b299eb0138d06a1e727 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
# make a link to this file if you are working hard in one directory of Coq
# ln -s ../dev/tools/Makefile.dir Makefile
# if you are working in a sub/dir/ make a link to dev/tools/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
|
