matita/components/Makefile

   1 H=@
   2 export SHELL=/bin/bash
   3
   4 include ../Makefile.defs
   5
   6 # Warning: the modules must be in compilation order
   7 NULL =
   8 MODULES =                       \
   9         extlib                  \
  10         xml                     \
  11         registry                \
  12         syntax_extensions       \
  13         thread                  \
  14         logger                  \
  15         ng_kernel               \
  16         ng_extraction           \
  17         getter                  \
  18         library                 \
  19         content                 \
  20         grafite                 \
  21         ng_refiner              \
  22         ng_library              \
  23         ng_cic_content          \
  24         disambiguation          \
  25         ng_disambiguation       \
  26         ng_paramodulation       \
  27         content_pres            \
  28         grafite_parser          \
  29         ng_tactics              \
  30         grafite_engine          \
  31         $(NULL)
  32
  33 METAS = $(MODULES:%=METAS/META.helm-%)
  34
  35 ifeq ($(DISTRIBUTED),no)
  36         MODULES+=binaries
  37 endif
  38
  39 all: metas $(MODULES:%=rec@all@%)
  40 opt: metas syntax-extensions $(MODULES:%=rec@opt@%)
  41
  42 ifeq ($(HAVE_OCAMLOPT),yes)
  43 world: opt
  44 else
  45 world: all
  46 endif
  47 syntax-extensions:
  48         $(H)$(MAKE) -C syntax_extensions depend
  49         $(H)$(MAKE) -C syntax_extensions
  50 depend: syntax-extensions $(MODULES:%=rec@depend@%)
  51 depend.opt: syntax-extensions $(MODULES:%=rec@depend.opt@%)
  52 install-arch: $(MODULES:%=rec@install@%)
  53 install-indep:
  54 uninstall: $(MODULES:%=rec@uninstall@%)
  55 clean: $(MODULES:%=rec@clean@%) clean_metas
  56
  57 .stats: $(MODULES:%=rec@.stats@%)
  58         $(H)(for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \
  59          | sort -t : -k 2 -n -r > .stats
  60
  61 rec@%:
  62         $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
  63
  64 EXTRA_DIST_CLEAN = \
  65         libraries-clusters.ps   \
  66         libraries-clusters.pdf  \
  67         libraries-ext.ps        \
  68         libraries.ps            \
  69         .dep.dot                \
  70         .extdep.dot             \
  71         .clustersdep.dot        \
  72         $(NULL)
  73
  74 distclean: clean clean_metas
  75         $(H)rm -f $(METAS)
  76         $(H)rm -f configure config.log config.cache config.status
  77         $(H)rm -f $(EXTRA_DIST_CLEAN)
  78
  79 .PHONY: all opt world metas depend install uninstall clean clean_metas distclean
  80
  81 METAS/META.helm-%: METAS/meta.helm-%.src
  82         $(H)cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
  83
  84 SIMPLIFYDEPS = ../daemons/graphs/tools/simplify_deps/simplify_deps
  85 $(SIMPLIFYDEPS):
  86         $(H)$(MAKE) -C $(dir $(SIMPLIFYDEPS))
  87
  88 .PHONY: .dep.dot
  89 .dep.dot: $(SIMPLIFYDEPS)
  90         $(H)echo "digraph G {" > $@
  91         $(H)echo "   rankdir = TB ;" >> $@
  92         $(H)for i in $(MODULES); do \
  93                 $(OCAMLFIND) query helm-$$i -recursive -p-format | \
  94                 grep helm | \
  95                 sed "s/^helm-/ \"$$i\" -> \"/g" | \
  96                 sed "s/$$/\";/g" >> $@ ; \
  97         done
  98         $(H)mv $@ $@.old ; $(SIMPLIFYDEPS) < $@.old > $@ ; rm $@.old
  99         $(H)echo "}" >> $@
 100
 101 .PHONY: .alldep.dot
 102 .alldep.dot:
 103         $(H)echo "digraph G {" > $@
 104         $(H)echo "   rankdir = TB ;" >> $@
 105         $(H)for i in $(MODULES); do \
 106                 $(OCAMLFIND) query helm-$$i -recursive -p-format | \
 107                         grep -v "pxp-" | \
 108                         sed "s/^pxp/pxp[-*]/g" | \
 109                         sed "s/^/ \"helm-$$i\" -> \"/g" | \
 110                         sed "s/$$/\";/g" >> $@ ; \
 111         done
 112         $(H)mv $@ $@.old ; \
 113                 ./simplify_deps/simplify_deps.opt < $@.old > $@ ; \
 114                 rm $@.old
 115         $(H)for i in $(MODULES); do \
 116                 echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];"\
 117                         >> $@ ; \
 118         done
 119         $(H)echo "}" >> $@
 120
 121 .extdep.dot: .dep.dot
 122         $(H)STATS/patch_deps.sh $< $@
 123 .clustersdep.dot: .dep.dot
 124         $(H)USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
 125
 126 libraries.ps: .dep.dot
 127         $(H)dot -Tps -o $@ $<
 128 libraries-ext.ps: .extdep.dot
 129         $(H)dot -Tps -o $@ $<
 130 libraries-clusters.ps: .clustersdep.dot
 131         $(H)dot -Tps -o $@ $<
 132 libraries-complete.ps: .alldep.dot
 133         $(H)dot -Tps -o $@ $<
 134
 135 ps: libraries.ps libraries-ext.ps libraries-clusters.ps
 136
 137 tags: TAGS
 138 .PHONY: TAGS
 139 TAGS:
 140         $(H)otags -vi -r .
 141
 142 metas: $(filter-out METAS/META.helm-binaries, $(METAS))