]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/Makefile
new tactics are almost ready
[helm.git] / helm / software / 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         cic_exportation         \
24         metadata                \
25         library                 \
26         acic_content            \
27         grafite                 \
28         content_pres            \
29         cic_unification         \
30         whelp                   \
31         tactics                 \
32         acic_procedural         \
33         disambiguation  \
34         cic_disambiguation      \
35         lexicon                 \
36         ng_kernel               \
37         ng_refiner              \
38         ng_disambiguation       \
39         grafite_parser          \
40         ng_tactics              \
41         grafite_engine          \
42         tptp_grafite            \
43         $(NULL)
44
45 METAS = $(MODULES:%=METAS/META.helm-%)
46
47 ifeq ($(DISTRIBUTED),no)
48         MODULES+=binaries
49 endif
50
51 all: metas $(MODULES:%=rec@all@%) 
52 opt: metas syntax-extensions $(MODULES:%=rec@opt@%)
53
54 ifeq ($(HAVE_OCAMLOPT),yes)
55 world: opt
56 else
57 world: all
58 endif
59 syntax-extensions:
60         $(H)$(MAKE) -C syntax_extensions depend
61         $(H)$(MAKE) -C syntax_extensions
62 depend: syntax-extensions $(MODULES:%=rec@depend@%)
63 depend.opt: syntax-extensions $(MODULES:%=rec@depend.opt@%)
64 install-arch: $(MODULES:%=rec@install@%)
65 install-indep:
66 uninstall: $(MODULES:%=rec@uninstall@%)
67 clean: $(MODULES:%=rec@clean@%) clean_metas
68
69 .stats: $(MODULES:%=rec@.stats@%)
70         $(H)(for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \
71          | sort -t : -k 2 -n -r > .stats
72
73 rec@%:
74         $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
75
76 EXTRA_DIST_CLEAN = \
77         libraries-clusters.ps   \
78         libraries-clusters.pdf  \
79         libraries-ext.ps        \
80         libraries.ps            \
81         .dep.dot                \
82         .extdep.dot             \
83         .clustersdep.dot        \
84         $(NULL)
85
86 distclean: clean clean_metas
87         $(H)rm -f $(METAS)
88         $(H)rm -f configure config.log config.cache config.status
89         $(H)rm -f $(EXTRA_DIST_CLEAN)
90
91 .PHONY: all opt world metas depend install uninstall clean clean_metas distclean
92
93 METAS/META.helm-%: METAS/meta.helm-%.src
94         $(H)cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
95
96 SIMPLIFYDEPS = ../daemons/graphs/tools/simplify_deps/simplify_deps
97 $(SIMPLIFYDEPS):
98         $(H)$(MAKE) -C $(dir $(SIMPLIFYDEPS))
99
100 .PHONY: .dep.dot
101 .dep.dot: $(SIMPLIFYDEPS)
102         $(H)echo "digraph G {" > $@
103         $(H)echo "   rankdir = TB ;" >> $@
104         $(H)for i in $(MODULES); do \
105                 $(OCAMLFIND) query helm-$$i -recursive -p-format | \
106                 grep helm | \
107                 sed "s/^helm-/ \"$$i\" -> \"/g" | \
108                 sed "s/$$/\";/g" >> $@ ; \
109         done
110         $(H)mv $@ $@.old ; $(SIMPLIFYDEPS) < $@.old > $@ ; rm $@.old
111         $(H)echo "}" >> $@
112
113 .PHONY: .alldep.dot
114 .alldep.dot:
115         $(H)echo "digraph G {" > $@
116         $(H)echo "   rankdir = TB ;" >> $@
117         $(H)for i in $(MODULES); do \
118                 $(OCAMLFIND) query helm-$$i -recursive -p-format | \
119                         grep -v "pxp-" | \
120                         sed "s/^pxp/pxp[-*]/g" | \
121                         sed "s/^/ \"helm-$$i\" -> \"/g" | \
122                         sed "s/$$/\";/g" >> $@ ; \
123         done
124         $(H)mv $@ $@.old ; \
125                 ./simplify_deps/simplify_deps.opt < $@.old > $@ ; \
126                 rm $@.old
127         $(H)for i in $(MODULES); do \
128                 echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];"\
129                         >> $@ ; \
130         done
131         $(H)echo "}" >> $@
132
133 .extdep.dot: .dep.dot
134         $(H)STATS/patch_deps.sh $< $@
135 .clustersdep.dot: .dep.dot
136         $(H)USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
137
138 libraries.ps: .dep.dot
139         $(H)dot -Tps -o $@ $<
140 libraries-ext.ps: .extdep.dot
141         $(H)dot -Tps -o $@ $<
142 libraries-clusters.ps: .clustersdep.dot
143         $(H)dot -Tps -o $@ $<
144 libraries-complete.ps: .alldep.dot
145         $(H)dot -Tps -o $@ $<
146
147 ps: libraries.ps libraries-ext.ps libraries-clusters.ps
148
149 tags: TAGS
150 .PHONY: TAGS
151 TAGS:
152         $(H)otags -vi -r .
153
154 metas: $(filter-out METAS/META.helm-binaries, $(METAS))