X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fuse_case%2Fstats%2FMakefile;h=6858eb6373082f3041ef1568526507722462a3cd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6db5d94691cfb9c3cddf30554c62b3a28b9974c0;hpb=d0db96d10fc88ad78e1e913d1b8a67e41f6bb976;p=helm.git

diff --git a/helm/papers/use_case/stats/Makefile b/helm/papers/use_case/stats/Makefile
index 6db5d9469..6858eb637 100644
--- a/helm/papers/use_case/stats/Makefile
+++ b/helm/papers/use_case/stats/Makefile
@@ -1,15 +1,116 @@
 
+SORT_SIZE = sort -n
+
+SORT_NODES = sort -t ' ' -k 2 -n
+
+TARGETS = con ind var body types proof_tree
+
+STATS_TARGETS = \
+  $(TARGETS:%=stats_%.xml) \
+  stats_theories.xml
+
+all_xml: $(STATS_TARGETS)
+
+all_html: $(STATS_TARGETS:%.xml=%.html)
+
+all_txt: $(STATS_TARGETS:%.xml=%.txt)
+
 stats: stats.cc
 	g++ -o $@ `pkg-config gdome2-cpp-smart --cflags --libs` $<
 
-stats.xml:
-	echo "<statistics>" >stats.xml
-	find /local/helm/library/coq_contribs/$(CONTRIB) -type f -exec ./stats.sh {} \; >>stats.xml
-	echo "</statistics>" >>stats.xml
+#%.xml.gz: %.xml
+#	gzip $<
+
+stats_%.xml.gz: stats_%.xml
+	gzip $<
+
+stats_%.xml:
+	@echo "<statistics>" >$@
+	@find /local/helm/library/coq_contribs/$(CONTRIB) -name "*."$(@:stats_%.xml=%)".xml.gz" -type f -exec ./stats.sh {} \; >>$@
+	@echo "</statistics>" >>$@
 
-stats.html: stats.xml
+stats_theories.xml:
+	@echo "<statistics>" >$@
+	@find /local/helm/library/theories -name "*.xml" -type f -exec ./stats.sh {} \; >>$@
+	@echo "</statistics>" >>$@
+
+stats_%.html: stats_%.xml.gz
 	xsltproc mkhtml.xsl $< >$@
 
-stats.txt: stats.html
-	w3m -dump a.html > a.txt
+stats_%.txt: stats_%.xml.gz extract.xsl
+	xsltproc extract.xsl $< >$@
+
+stats_candidates.xml.gz:
+	./stats_candidates.sh
+	
+stats_candidates_c1.xml.gz:
+	./stats_candidates_c1.sh
+
+mkdiff: mkdiff.cc
+	g++ -o $@ $<
+
+parsing_times_%_candidates.txt: parsing_times.sh stats_candidates.txt
+	@echo "Collecting parsing times in CICXML_NOBLANKS_NODTD for $(@:parsing_times_%_candidates.txt=%)..."
+	@./$< CICXML_NOBLANKS_NODTD parsing_time_$(@:parsing_times_%_candidates.txt=%).sh stats_candidates.txt | $(SORT_NODES) >$@
+
+parsing_times_%_candidates_c1.txt: parsing_times.sh stats_candidates_c1.txt
+	@echo "Collecting parsing times in CONTENTNB for $(@:parsing_times_%_candidates_c1.txt=%)..."
+	@./$< CONTENTNB parsing_time_$(@:parsing_times_%_candidates_c1.txt=%).sh stats_candidates_c1.txt | $(SORT_NODES) >$@
+
+#parsing_times_%_candidates: parsing_times_%_candidates.sh
+#	sh $< >$@
+
+#parsing_times_%_candidates_c1: parsing_times_%_candidates_c1.sh
+#	sh $< >$@
+
+PARSING_TIMES_TARGETS = libxml2_reader libxml2_sax2 libxml2_tree expat xerces_sax2 xerces_tree
+
+PARSING_TIMES_TARGETS_TXT = \
+  $(PARSING_TIMES_TARGETS:%=parsing_times_%_candidates.txt) \
+  $(PARSING_TIMES_TARGETS:%=parsing_times_%_candidates_c1.txt)
+
+parsing_times_candidates.ps parsing_times_candidates_c1.ps: $(PARSING_TIMES_TARGETS_TXT) parsing_times.gpscript
+	gnuplot parsing_times.gpscript
+
+parsing_times: parsing_times_candidates.ps parsing_times_candidates_c1.ps
+
+stats_candidates_localdtd.txt: stats_candidates.txt
+	sed s/_NODTD/_LOCALDTD/ $< >$@
+
+parsing_validating_times_%_candidates.txt: validating_times.sh stats_candidates_localdtd.txt
+	@echo "Collecting validating times in CICXML_NOBLANKS_LOCALDTD for $(@:parsing_validating_times_%_candidates.txt=%)..."
+	@./$< CICXML_NOBLANKS_LOCALDTD validating_time_$(@:parsing_validating_times_%_candidates.txt=%).sh stats_candidates_localdtd.txt | $(SORT_NODES) >$@
+
+PARSING_VALIDATING_TIMES_TARGETS = libxml2_tree xerces_sax2 xerces_tree flea
+
+PARSING_VALIDATING_TIMES_TARGETS_TXT = \
+  $(PARSING_VALIDATING_TIMES_TARGETS:%=parsing_validating_times_%_candidates.txt)
+
+validating_times_libxml2_tree_candidates.txt: parsing_validating_times_libxml2_tree_candidates.txt parsing_times_libxml2_tree_candidates.txt
+	@$(SORT_NODES) parsing_times_libxml2_tree_candidates.txt | ./mkdiff $^ >$@
+
+validating_times_xerces_sax2_candidates.txt: parsing_validating_times_xerces_sax2_candidates.txt parsing_times_xerces_sax2_candidates.txt
+	@$(SORT_NODES) parsing_times_xerces_sax2_candidates.txt | ./mkdiff $^ >$@
+
+validating_times_xerces_tree_candidates.txt: parsing_validating_times_xerces_tree_candidates.txt parsing_times_xerces_tree_candidates.txt
+	@$(SORT_NODES) parsing_times_xerces_tree_candidates.txt | ./mkdiff $^ >$@
+
+validating_times_flea_candidates.txt: parsing_validating_times_flea_candidates.txt parsing_times_libxml2_sax2_candidates.txt
+	@$(SORT_NODES) parsing_times_libxml2_sax2_candidates.txt | ./mkdiff $^ >$@
+
+VALIDATING_TIMES_TARGETS = libxml2_tree xerces_sax2 xerces_tree flea
+
+VALIDATING_TIMES_TARGETS_TXT = \
+  $(VALIDATING_TIMES_TARGETS:%=validating_times_%_candidates.txt)
+
+parsing_validating_times_candidates.ps validating_times_candidates.ps: $(VALIDATING_TIMES_TARGETS_TXT) $(PARSING_VALIDATING_TIMES_TARGETS_TXT) validating_times.gpscript
+	gnuplot validating_times.gpscript
+
+validating_times: parsing_validating_times_candidates.ps validating_times_candidates.ps
+
+clean:
+	rm -f stats_candidates*.{xml,html,txt} \
+	  $(PARSING_TIMES_TARGETS_TXT) \
+	  $(PARSING_VALIDATING_TIMES_TARGETS_TXT) \
+	  $(VALIDATING_TIMES_TARGETS_TXT)