]> matita.cs.unibo.it Git - helm.git/blob - components/Makefile
we started the infrastructure for the procedural rendering of proofs
[helm.git] / components / Makefile
1 H=@
2 export SHELL=/bin/bash
3
4 include ../Makefile.defs
5
6 # Warning: the modules must be in compilation order
7 NULL =
8 MODULES =                       \
9         extlib                  \
10         xml                     \
11         hgdome                  \
12         registry                \
13         hmysql                  \
14         syntax_extensions \
15         thread                  \
16         xmldiff                 \
17         urimanager              \
18         logger                  \
19         getter                  \
20         cic                     \
21         cic_proof_checking      \
22         cic_acic                \
23         metadata                \
24         library                 \
25         acic_content            \
26         grafite                 \
27         content_pres            \
28         cic_unification         \
29         whelp                   \
30         tactics                 \
31         cic_disambiguation      \
32         lexicon                 \
33         grafite_engine          \
34         grafite_parser          \
35         tptp_grafite            \
36         $(NULL)
37
38 METAS = $(MODULES:%=METAS/META.helm-%)
39
40 ifeq ($(DISTRIBUTED),no)
41         MODULES+=binaries
42 endif
43
44 all: metas $(MODULES:%=rec@all@%) 
45 opt: metas $(MODULES:%=rec@opt@%)
46
47 ifeq ($(HAVE_OCAMLOPT),yes)
48 world: opt
49 else
50 world: all
51 endif
52 syntax-extensions:
53         $(H)$(MAKE) -C syntax_extensions depend
54         $(H)$(MAKE) -C syntax_extensions
55 depend: syntax-extensions $(MODULES:%=rec@depend@%)
56 depend.opt: syntax-extensions $(MODULES:%=rec@depend.opt@%)
57 install: $(MODULES:%=rec@install@%)
58 uninstall: $(MODULES:%=rec@uninstall@%)
59 clean: $(MODULES:%=rec@clean@%) clean_metas
60
61 .stats: $(MODULES:%=rec@.stats@%)
62         $(H)(for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \
63          | sort -t : -k 2 -n -r > .stats
64
65 rec@%:
66         $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
67
68 EXTRA_DIST_CLEAN = \
69         libraries-clusters.ps   \
70         libraries-clusters.pdf  \
71         libraries-ext.ps        \
72         libraries.ps            \
73         .dep.dot                \
74         .extdep.dot             \
75         .clustersdep.dot        \
76         $(NULL)
77
78 distclean: clean clean_metas
79         $(H)rm -f $(METAS)
80         $(H)rm -f configure config.log config.cache config.status
81         $(H)rm -f $(EXTRA_DIST_CLEAN)
82
83 .PHONY: all opt world metas depend install uninstall clean clean_metas distclean
84
85 METAS/META.helm-%: METAS/meta.helm-%.src
86         $(H)cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
87
88 SIMPLIFYDEPS = ../daemons/graphs/tools/simplify_deps/simplify_deps
89 $(SIMPLIFYDEPS):
90         $(H)$(MAKE) -C $(dir $(SIMPLIFYDEPS))
91
92 .PHONY: .dep.dot
93 .dep.dot: $(SIMPLIFYDEPS)
94         $(H)echo "digraph G {" > $@
95         $(H)echo "   rankdir = TB ;" >> $@
96         $(H)for i in $(MODULES); do \
97                 $(OCAMLFIND) query helm-$$i -recursive -p-format | \
98                 grep helm | \
99                 sed "s/^helm-/ \"$$i\" -> \"/g" | \
100                 sed "s/$$/\";/g" >> $@ ; \
101         done
102         $(H)mv $@ $@.old ; $(SIMPLIFYDEPS) < $@.old > $@ ; rm $@.old
103         $(H)echo "}" >> $@
104
105 .PHONY: .alldep.dot
106 .alldep.dot:
107         $(H)echo "digraph G {" > $@
108         $(H)echo "   rankdir = TB ;" >> $@
109         $(H)for i in $(MODULES); do \
110                 $(OCAMLFIND) query helm-$$i -recursive -p-format | \
111                         grep -v "pxp-" | \
112                         sed "s/^pxp/pxp[-*]/g" | \
113                         sed "s/^/ \"helm-$$i\" -> \"/g" | \
114                         sed "s/$$/\";/g" >> $@ ; \
115         done
116         $(H)mv $@ $@.old ; \
117                 ./simplify_deps/simplify_deps.opt < $@.old > $@ ; \
118                 rm $@.old
119         $(H)for i in $(MODULES); do \
120                 echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];"\
121                         >> $@ ; \
122         done
123         $(H)echo "}" >> $@
124
125 .extdep.dot: .dep.dot
126         $(H)STATS/patch_deps.sh $< $@
127 .clustersdep.dot: .dep.dot
128         $(H)USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
129
130 libraries.ps: .dep.dot
131         $(H)dot -Tps -o $@ $<
132 libraries-ext.ps: .extdep.dot
133         $(H)dot -Tps -o $@ $<
134 libraries-clusters.ps: .clustersdep.dot
135         $(H)dot -Tps -o $@ $<
136 libraries-complete.ps: .alldep.dot
137         $(H)dot -Tps -o $@ $<
138
139 ps: libraries.ps libraries-ext.ps libraries-clusters.ps
140
141 tags: TAGS
142 .PHONY: TAGS
143 TAGS:
144         $(H)otags -vi -r .
145
146 metas: $(filter-out METAS/META.helm-binaries, $(METAS))