+
+export SHELL=/bin/bash
+
+include ../Makefile.defs
+
# Warning: the modules must be in compilation order
-MODULES= xml urimanager getter pxp cic cic_annotations cic_annotations_cache \
- cic_cache cic_proof_checking
+NULL =
+MODULES = \
+ extlib \
+ xml \
+ hgdome \
+ registry \
+ hmysql \
+ utf8_macros \
+ thread \
+ xmldiff \
+ urimanager \
+ logger \
+ getter \
+ cic \
+ cic_proof_checking \
+ cic_acic \
+ acic_content \
+ content_pres \
+ grafite \
+ metadata \
+ library \
+ cic_unification \
+ whelp \
+ tactics \
+ cic_disambiguation \
+ lexicon \
+ grafite_engine \
+ grafite_parser \
+ tactics/paramodulation \
+ $(NULL)
+
+METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%))
+
+all: metas $(MODULES:%=%.all)
+opt: metas $(MODULES:%=%.opt)
+world: all opt
+depend: $(MODULES:%=%.depend)
+install: $(MODULES:%=%.install)
+uninstall: $(MODULES:%=%.uninstall)
+clean: $(MODULES:%=%.clean) clean_metas
+
+.stats: $(MODULES:%=%.stats)
+ (for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \
+ | sort -t : -k 2 -n -r > .stats
+
+EXTRA_DIST_CLEAN = \
+ libraries-clusters.ps \
+ libraries-clusters.pdf \
+ libraries-ext.ps \
+ libraries.ps \
+ .dep.dot \
+ .extdep.dot \
+ .clustersdep.dot \
+ $(NULL)
+
+distclean: clean clean_metas
+ rm -f $(METAS)
+ rm -f configure config.log config.cache config.status
+ rm -f Makefile Makefile.common $(EXTRA_DIST_CLEAN)
+
+.PHONY: all opt world metas depend install uninstall clean clean_metas distclean
+
+%.all:
+ $(MAKE) -C $* all
+%.opt:
+ $(MAKE) -C $* opt
+%.clean:
+ $(MAKE) -C $* clean
+%.depend:
+ $(MAKE) -C $* depend
+%.stats:
+ @$(MAKE) -C $* .stats
+%.install:
+ $(MAKE) -C $* install
+%.uninstall:
+ $(MAKE) -C $* uninstall
+
+METAS/META.helm-%: METAS/meta.helm-%.src
+ cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
+
+.PHONY: .dep.dot
+.dep.dot:
+ echo "digraph G {" > $@
+ echo " rankdir = TB ;" >> $@
+ for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep helm | sed "s/^helm-/ \"$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done
+ mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
+ echo "}" >> $@
+
+.PHONY: .alldep.dot
+.alldep.dot:
+ echo "digraph G {" > $@
+ echo " rankdir = TB ;" >> $@
+ for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep -v "pxp-" | sed "s/^pxp/pxp[-*]/g" | sed "s/^/ \"helm-$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done
+ mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
+ for i in $(MODULES); do echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];" >> $@ ; done
+ echo "}" >> $@
+
+.extdep.dot: .dep.dot
+ STATS/patch_deps.sh $< $@
+.clustersdep.dot: .dep.dot
+ USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
+
+libraries.ps: .dep.dot
+ dot -Tps -o $@ $<
+libraries-ext.ps: .extdep.dot
+ dot -Tps -o $@ $<
+libraries-clusters.ps: .clustersdep.dot
+ dot -Tps -o $@ $<
+libraries-complete.ps: .alldep.dot
+ dot -Tps -o $@ $<
+
+ps: libraries.ps libraries-ext.ps libraries-clusters.ps
+
+tags: TAGS
+.PHONY: TAGS
+TAGS:
+ otags -vi -r .
-all opt depend install uninstall clean:
- for i in $(MODULES) ; do (cd $$i ; make $@) ; done