* snapshot

[helm.git] / helm / papers / use_case / stats / Makefile

diff --git a/helm/papers/use_case/stats/Makefile b/helm/papers/use_case/stats/Makefile
index fa5f5e2e907ec882e5cbf0b1a9c4b6dff2a395b7..fdfdb9ff09078f92d14ad6eee604df5945815e8c 100644 (file)
--- a/helm/papers/use_case/stats/Makefile
+++ b/helm/papers/use_case/stats/Makefile
@@ -1,4 +1,31 @@
 
+TARGETS = con ind var body types proof_tree
+
+STATS_TARGETS = \
+  $(TARGETS:%=stats_%.xml) \
+  stats_theories.xml
+
+all: $(STATS_TARGETS)
+
 stats: stats.cc
        g++ -o $@ `pkg-config gdome2-cpp-smart --cflags --libs` $<
 
+stats_%.xml:
+       @echo "<statistics>" >$@
+       @find /local/helm/library/coq_contribs/$(CONTRIB) -name "*."$(@:stats_%.xml=%)".xml.gz" -type f -exec ./stats.sh {} \; >>$@
+       @echo "</statistics>" >>$@
+
+stats_theories.xml:
+       @echo "<statistics>" >$@
+       @find /local/helm/library/theories -name "*.xml" -type f -exec ./stats.sh {} \; >>$@
+       @echo "</statistics>" >>$@
+
+stats_%.html: stats_%.xml
+       xsltproc mkhtml.xsl $< >$@
+
+stats_%.txt: stats_%.html
+       w3m -cols 132 -dump $< >$@
+
+clean:
+       rm -f stats.{xml,html,txt}
+