*** Very experimental and not branched ***

[helm.git] / components / Makefile

diff --git a/components/Makefile b/components/Makefile
index c16dc0e714fc20cb27c827d2eec83af70e8378f5..34020150a7d746942017adff28502cd3606fbab2 100644 (file)
--- a/components/Makefile
+++ b/components/Makefile
@@ -1,4 +1,4 @@
-
+H=@
 export SHELL=/bin/bash
 
 include ../Makefile.defs
@@ -11,7 +11,7 @@ MODULES =                     \
        hgdome                  \
        registry                \
        hmysql                  \
-       utf8_macros             \
+       syntax_extensions \
        thread                  \
        xmldiff                 \
        urimanager              \
@@ -19,44 +19,54 @@ MODULES =                   \
        getter                  \
        cic                     \
        cic_proof_checking      \
+       cic_exportation         \
        cic_acic                \
-       acic_content            \
-       content_pres            \
-       grafite                 \
        metadata                \
        library                 \
+       acic_content            \
+       grafite                 \
+       content_pres            \
        cic_unification         \
        whelp                   \
        tactics                 \
+       acic_procedural         \
        cic_disambiguation      \
        lexicon                 \
        grafite_engine          \
        grafite_parser          \
-       tactics/paramodulation  \
+       tptp_grafite            \
        $(NULL)
 
-METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%))
+METAS = $(MODULES:%=METAS/META.helm-%)
+
+ifeq ($(DISTRIBUTED),no)
+       MODULES+=binaries
+endif
 
 all: metas $(MODULES:%=rec@all@%) 
-opt: metas $(MODULES:%=rec@opt@%)
+opt: metas syntax-extensions $(MODULES:%=rec@opt@%)
+
 ifeq ($(HAVE_OCAMLOPT),yes)
-world: all opt
+world: opt
 else
 world: all
 endif
-depend: $(MODULES:%=rec@depend@%)
-install: $(MODULES:%=rec@install@%)
+syntax-extensions:
+       $(H)$(MAKE) -C syntax_extensions depend
+       $(H)$(MAKE) -C syntax_extensions
+depend: syntax-extensions $(MODULES:%=rec@depend@%)
+depend.opt: syntax-extensions $(MODULES:%=rec@depend.opt@%)
+install-arch: $(MODULES:%=rec@install@%)
+install-indep:
 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) \
+       $(H)(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 @, ,$*))
+       $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
 
 EXTRA_DIST_CLEAN = \
        libraries-clusters.ps   \
@@ -69,50 +79,71 @@ EXTRA_DIST_CLEAN = \
        $(NULL)
 
 distclean: clean clean_metas
-       rm -f $(METAS)
-       rm -f configure config.log config.cache config.status
-       rm -f $(EXTRA_DIST_CLEAN)
+       $(H)rm -f $(METAS)
+       $(H)rm -f configure config.log config.cache config.status
+       $(H)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)/$*\"" >> $@
+       $(H)cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
+
+SIMPLIFYDEPS = ../daemons/graphs/tools/simplify_deps/simplify_deps
+$(SIMPLIFYDEPS):
+       $(H)$(MAKE) -C $(dir $(SIMPLIFYDEPS))
 
 .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 "}" >> $@
+.dep.dot: $(SIMPLIFYDEPS)
+       $(H)echo "digraph G {" > $@
+       $(H)echo "   rankdir = TB ;" >> $@
+       $(H)for i in $(MODULES); do \
+               $(OCAMLFIND) query helm-$$i -recursive -p-format | \
+               grep helm | \
+               sed "s/^helm-/ \"$$i\" -> \"/g" | \
+               sed "s/$$/\";/g" >> $@ ; \
+       done
+       $(H)mv $@ $@.old ; $(SIMPLIFYDEPS) < $@.old > $@ ; rm $@.old
+       $(H)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 "}" >> $@
+       $(H)echo "digraph G {" > $@
+       $(H)echo "   rankdir = TB ;" >> $@
+       $(H)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
+       $(H)mv $@ $@.old ; \
+               ./simplify_deps/simplify_deps.opt < $@.old > $@ ; \
+               rm $@.old
+       $(H)for i in $(MODULES); do \
+               echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];"\
+                       >> $@ ; \
+       done
+       $(H)echo "}" >> $@
 
 .extdep.dot: .dep.dot
-       STATS/patch_deps.sh $< $@
+       $(H)STATS/patch_deps.sh $< $@
 .clustersdep.dot: .dep.dot
-       USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
+       $(H)USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
 
 libraries.ps: .dep.dot
-       dot -Tps -o $@ $<
+       $(H)dot -Tps -o $@ $<
 libraries-ext.ps: .extdep.dot
-       dot -Tps -o $@ $<
+       $(H)dot -Tps -o $@ $<
 libraries-clusters.ps: .clustersdep.dot
-       dot -Tps -o $@ $<
+       $(H)dot -Tps -o $@ $<
 libraries-complete.ps: .alldep.dot
-       dot -Tps -o $@ $<
+       $(H)dot -Tps -o $@ $<
 
 ps: libraries.ps libraries-ext.ps libraries-clusters.ps
 
 tags: TAGS
 .PHONY: TAGS
 TAGS:
-       otags -vi -r .
+       $(H)otags -vi -r .
 
+metas: $(filter-out METAS/META.helm-binaries, $(METAS))