export SHELL=/bin/bash include ../Makefile.defs # Warning: the modules must be in compilation order NULL = MODULES = \ extlib \ xml \ hgdome \ registry \ hmysql \ utf8_macros \ thread \ xmldiff \ urimanager \ logger \ getter \ cic \ cic_proof_checking \ cic_acic \ metadata \ library \ acic_content \ content_pres \ grafite \ 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:%=rec@all@%) opt: metas $(MODULES:%=rec@opt@%) ifeq ($(HAVE_OCAMLOPT),yes) world: all opt else world: all endif depend: $(MODULES:%=rec@depend@%) install: $(MODULES:%=rec@install@%) uninstall: $(MODULES:%=rec@uninstall@%) clean: $(MODULES:%=rec@clean@%) clean_metas .stats: $(MODULES:%=rec@.stats@%) (for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \ | sort -t : -k 2 -n -r > .stats rec@%@tactics/paramodulation: $(MAKE) -C tactics/paramodulation $* rec@%: $(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) 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 $(EXTRA_DIST_CLEAN) .PHONY: all opt world metas depend install uninstall clean clean_metas distclean 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 .