X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2FMakefile.in;h=7ab72ed248e92a87909210f66dd8b20ca7397834;hb=782253ebe87375f52c07899c1501db5a665a457f;hp=02d81d265f58a8f762c468e6554db749f666c290;hpb=ef5ed8ca675b0cbc6604ffbecd23cc3b28982863;p=helm.git diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 02d81d265..7ab72ed24 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -1,71 +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 \ - cic_textual_parser \ - cic_textual_parser2 \ - tex_cic_textual_parser \ - cic_unification \ - mathql \ - mathql_generator \ - mathql_interpreter \ - cic_omdoc \ - tactics \ - cic_transformations \ - logger +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) OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ -OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ +OCAMLPATH = @OCAMLFIND_META_DIR@ +OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@ -METAS = $(MODULES:%=METAS/META.helm-%) -CWD=`pwd` +METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%)) -all: metas $(MODULES:%=%.all) +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_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) -dist-clean: clean - rm -f Makefile Makefile.common configure config.log config.cache config.status +.PHONY: all opt world metas depend install uninstall clean clean_metas distclean + +%.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 export TARGET=$(OCAMLFIND_META_DIR)/$(@:%.install=META.helm-%) ; \ - cp $(@:%.install=META.helm-%.src) $$TARGET && \ + cp METAS/$(@:%.install=meta.helm-%.src) $$TARGET && \ echo "directory=\"$(OCAMLFIND_DEST_DIR)/$(@:%.install=%)\"" >> $$TARGET $(MODULES:%=%.uninstall): cd $(@:%.uninstall=%) && make uninstall rm -f $(OCAMLFIND_META_DIR)/$(@:%.uninstall=META.helm-%) -$(MODULES:%=%.clean): - cd $(@:%.clean=%) && make clean METAS/META.helm-%: METAS/meta.helm-%.src - cp $< $@ && echo "directory=\"$(CWD)/$*\"" >> $@ + 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 + 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 . +