blob: 80fe5834c6c7af3791ba52eab76786b5c9471cb4 (
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
|
# 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/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)
FORCE:
clean::
rm -f *.ml.mli
# this is not perfect but mostly WORKS! It just calls the main makefile
%.cmi: *.mli
$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
SOURCES=$(wildcard *.mli) $(wildcard *.ml) $(wildcard *.ml4)
%.cmo: $(SOURCES)
$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
coqtop:
$(MAKE) -C $(TOPDIR) bin/coqtop.byte
|
