helm/ocaml/Makefile

   1
   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         hgdome                  \
  12         registry                \
  13         hmysql                  \
  14         utf8_macros             \
  15         thread                  \
  16         xmldiff                 \
  17         urimanager              \
  18         logger                  \
  19         getter                  \
  20         cic                     \
  21         cic_proof_checking      \
  22         cic_acic                \
  23         acic_content            \
  24         content_pres            \
  25         grafite                 \
  26         metadata                \
  27         library                 \
  28         cic_unification         \
  29         whelp                   \
  30         tactics                 \
  31         cic_disambiguation      \
  32         lexicon                 \
  33         grafite_engine          \
  34         grafite_parser          \
  35         tactics/paramodulation  \
  36         $(NULL)
  37
  38 METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%))
  39
  40 all: metas $(MODULES:%=%.all)
  41 opt: metas $(MODULES:%=%.opt)
  42 world: all opt
  43 depend: $(MODULES:%=%.depend)
  44 install: $(MODULES:%=%.install)
  45 uninstall: $(MODULES:%=%.uninstall)
  46 clean: $(MODULES:%=%.clean) clean_metas
  47
  48 .stats: $(MODULES:%=%.stats)
  49         (for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \
  50          | sort -t : -k 2 -n -r > .stats
  51
  52 EXTRA_DIST_CLEAN = \
  53         libraries-clusters.ps   \
  54         libraries-clusters.pdf  \
  55         libraries-ext.ps        \
  56         libraries.ps            \
  57         .dep.dot                \
  58         .extdep.dot             \
  59         .clustersdep.dot        \
  60         $(NULL)
  61
  62 distclean: clean clean_metas
  63         rm -f $(METAS)
  64         rm -f configure config.log config.cache config.status
  65         rm -f $(EXTRA_DIST_CLEAN)
  66
  67 .PHONY: all opt world metas depend install uninstall clean clean_metas distclean
  68
  69 %.all:
  70         $(MAKE) -C $* all
  71 %.opt:
  72         $(MAKE) -C $* opt
  73 %.clean:
  74         $(MAKE) -C $* clean
  75 %.depend:
  76         $(MAKE) -C $* depend
  77 %.stats:
  78         @$(MAKE) -C $* .stats
  79 %.install:
  80         $(MAKE) -C $* install
  81 %.uninstall:
  82         $(MAKE) -C $* uninstall
  83
  84 METAS/META.helm-%: METAS/meta.helm-%.src
  85         cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
  86
  87 .PHONY: .dep.dot
  88 .dep.dot:
  89         echo "digraph G {" > $@
  90         echo "   rankdir = TB ;" >> $@
  91         for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep helm | sed "s/^helm-/ \"$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done
  92         mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
  93         echo "}" >> $@
  94
  95 .PHONY: .alldep.dot
  96 .alldep.dot:
  97         echo "digraph G {" > $@
  98         echo "   rankdir = TB ;" >> $@
  99         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
 100         mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
 101         for i in $(MODULES); do echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];" >> $@ ; done
 102         echo "}" >> $@
 103
 104 .extdep.dot: .dep.dot
 105         STATS/patch_deps.sh $< $@
 106 .clustersdep.dot: .dep.dot
 107         USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
 108
 109 libraries.ps: .dep.dot
 110         dot -Tps -o $@ $<
 111 libraries-ext.ps: .extdep.dot
 112         dot -Tps -o $@ $<
 113 libraries-clusters.ps: .clustersdep.dot
 114         dot -Tps -o $@ $<
 115 libraries-complete.ps: .alldep.dot
 116         dot -Tps -o $@ $<
 117
 118 ps: libraries.ps libraries-ext.ps libraries-clusters.ps
 119
 120 tags: TAGS
 121 .PHONY: TAGS
 122 TAGS:
 123         otags -vi -r .
 124