X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2FMakefile.in;h=7ab72ed248e92a87909210f66dd8b20ca7397834;hb=782253ebe87375f52c07899c1501db5a665a457f;hp=83b28f78cae475c6cff9495f6348e6ae861e1609;hpb=a6611bb09e2fa8629a022dbcd6c527ea8fd4df32;p=helm.git diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 83b28f78c..7ab72ed24 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,32 +1,132 @@ + +export SHELL=/bin/bash + # 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 = $(MODULES:%=META.helm-%) -CWD=`pwd` +OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ +OCAMLPATH = @OCAMLFIND_META_DIR@ +OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@ -all: $(METAS) $(MODULES:%=%.all) -opt: $(METAS) $(MODULES:%=%.opt) +METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%)) + +all: metas $(MODULES:%=%.all) +opt: metas $(MODULES:%=%.opt) +world: all opt +metas: $(METAS) depend: $(MODULES:%=%.depend) install: $(MODULES:%=%.install) uninstall: $(MODULES:%=%.uninstall) -clean: $(MODULES:%=%.clean) +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) + +clean_metas: rm -f $(METAS) +distclean: clean clean_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 -dist-clean: clean - rm -f Makefile configure config.log config.cache config.status +%.all: + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* all +%.opt: + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* opt +%.clean: + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* clean +%.depend: + @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* depend +%.stats: + @$(MAKE) -C $* .stats -$(MODULES:%=%.all): - export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.all=%) ; make all -$(MODULES:%=%.opt): - export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.opt=%) ; make opt -$(MODULES:%=%.depend): - export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.depend=%) ; make depend $(MODULES:%=%.install): - cd $(@:%.install=%) ; make install + cd $(@:%.install=%) && make install + export TARGET=$(OCAMLFIND_META_DIR)/$(@:%.install=META.helm-%) ; \ + cp METAS/$(@:%.install=meta.helm-%.src) $$TARGET && \ + echo "directory=\"$(OCAMLFIND_DEST_DIR)/$(@:%.install=%)\"" >> $$TARGET $(MODULES:%=%.uninstall): - cd $(@:%.uninstall=%) ; make uninstall -$(MODULES:%=%.clean): - cd $(@:%.clean=%) ; make clean -META.helm-%: META.helm-%.src - cp $< $@ ; echo "directory=\"$(CWD)/$(@:META.helm-%=%)\"" >> $@ + cd $(@:%.uninstall=%) && make uninstall + rm -f $(OCAMLFIND_META_DIR)/$(@:%.uninstall=META.helm-%) +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 . +