helm/papers/use_case/stats/Makefile

   1
   2 SORT_SIZE = sort -n
   3
   4 SORT_NODES = sort -t ' ' -k 2 -n
   5
   6 TARGETS = con ind var body types proof_tree
   7
   8 STATS_TARGETS = \
   9   $(TARGETS:%=stats_%.xml) \
  10   stats_theories.xml
  11
  12 all_xml: $(STATS_TARGETS)
  13
  14 all_html: $(STATS_TARGETS:%.xml=%.html)
  15
  16 all_txt: $(STATS_TARGETS:%.xml=%.txt)
  17
  18 stats: stats.cc
  19         g++ -o $@ `pkg-config gdome2-cpp-smart --cflags --libs` $<
  20
  21 #%.xml.gz: %.xml
  22 #       gzip $<
  23
  24 stats_%.xml.gz: stats_%.xml
  25         gzip $<
  26
  27 stats_%.xml:
  28         @echo "<statistics>" >$@
  29         @find /local/helm/library/coq_contribs/$(CONTRIB) -name "*."$(@:stats_%.xml=%)".xml.gz" -type f -exec ./stats.sh {} \; >>$@
  30         @echo "</statistics>" >>$@
  31
  32 stats_theories.xml:
  33         @echo "<statistics>" >$@
  34         @find /local/helm/library/theories -name "*.xml" -type f -exec ./stats.sh {} \; >>$@
  35         @echo "</statistics>" >>$@
  36
  37 stats_%.html: stats_%.xml.gz
  38         xsltproc mkhtml.xsl $< >$@
  39
  40 stats_%.txt: stats_%.xml.gz extract.xsl
  41         xsltproc extract.xsl $< >$@
  42
  43 stats_candidates.xml.gz:
  44         ./stats_candidates.sh
  45
  46 stats_candidates_c1.xml.gz:
  47         ./stats_candidates_c1.sh
  48
  49 mkdiff: mkdiff.cc
  50         g++ -o $@ $<
  51
  52 parsing_times_%_candidates.txt: parsing_times.sh stats_candidates.txt
  53         @echo "Collecting parsing times in CICXML_NOBLANKS_NODTD for $(@:parsing_times_%_candidates.txt=%)..."
  54         @./$< CICXML_NOBLANKS_NODTD parsing_time_$(@:parsing_times_%_candidates.txt=%).sh stats_candidates.txt | $(SORT_NODES) >$@
  55
  56 parsing_times_%_candidates_c1.txt: parsing_times.sh stats_candidates_c1.txt
  57         @echo "Collecting parsing times in CONTENTNB for $(@:parsing_times_%_candidates_c1.txt=%)..."
  58         @./$< CONTENTNB parsing_time_$(@:parsing_times_%_candidates_c1.txt=%).sh stats_candidates_c1.txt | $(SORT_NODES) >$@
  59
  60 #parsing_times_%_candidates: parsing_times_%_candidates.sh
  61 #       sh $< >$@
  62
  63 #parsing_times_%_candidates_c1: parsing_times_%_candidates_c1.sh
  64 #       sh $< >$@
  65
  66 PARSING_TIMES_TARGETS = libxml2_reader libxml2_sax2 libxml2_tree expat xerces_sax2 xerces_tree
  67
  68 PARSING_TIMES_TARGETS_TXT = \
  69   $(PARSING_TIMES_TARGETS:%=parsing_times_%_candidates.txt) \
  70   $(PARSING_TIMES_TARGETS:%=parsing_times_%_candidates_c1.txt)
  71
  72 parsing_times_candidates.ps parsing_times_candidates_c1.ps: $(PARSING_TIMES_TARGETS_TXT) parsing_times.gpscript
  73         gnuplot parsing_times.gpscript
  74
  75 parsing_times: parsing_times_candidates.ps parsing_times_candidates_c1.ps
  76
  77 stats_candidates_localdtd.txt: stats_candidates.txt
  78         sed s/_NODTD/_LOCALDTD/ $< >$@
  79
  80 parsing_validating_times_%_candidates.txt: validating_times.sh stats_candidates_localdtd.txt
  81         @echo "Collecting validating times in CICXML_NOBLANKS_LOCALDTD for $(@:parsing_validating_times_%_candidates.txt=%)..."
  82         @./$< CICXML_NOBLANKS_LOCALDTD validating_time_$(@:parsing_validating_times_%_candidates.txt=%).sh stats_candidates_localdtd.txt | $(SORT_NODES) >$@
  83
  84 PARSING_VALIDATING_TIMES_TARGETS = libxml2_tree xerces_sax2 xerces_tree flea
  85
  86 PARSING_VALIDATING_TIMES_TARGETS_TXT = \
  87   $(PARSING_VALIDATING_TIMES_TARGETS:%=parsing_validating_times_%_candidates.txt)
  88
  89 validating_times_libxml2_tree_candidates.txt: parsing_validating_times_libxml2_tree_candidates.txt parsing_times_libxml2_tree_candidates.txt
  90         @$(SORT_NODES) parsing_times_libxml2_tree_candidates.txt | ./mkdiff $^ >$@
  91
  92 validating_times_xerces_sax2_candidates.txt: parsing_validating_times_xerces_sax2_candidates.txt parsing_times_xerces_sax2_candidates.txt
  93         @$(SORT_NODES) parsing_times_xerces_sax2_candidates.txt | ./mkdiff $^ >$@
  94
  95 validating_times_xerces_tree_candidates.txt: parsing_validating_times_xerces_tree_candidates.txt parsing_times_xerces_tree_candidates.txt
  96         @$(SORT_NODES) parsing_times_xerces_tree_candidates.txt | ./mkdiff $^ >$@
  97
  98 validating_times_flea_candidates.txt: parsing_validating_times_flea_candidates.txt parsing_times_libxml2_sax2_candidates.txt
  99         @$(SORT_NODES) parsing_times_libxml2_sax2_candidates.txt | ./mkdiff $^ >$@
 100
 101 VALIDATING_TIMES_TARGETS = libxml2_tree xerces_sax2 xerces_tree flea
 102
 103 VALIDATING_TIMES_TARGETS_TXT = \
 104   $(VALIDATING_TIMES_TARGETS:%=validating_times_%_candidates.txt)
 105
 106 parsing_validating_times_candidates.ps validating_times_candidates.ps: $(VALIDATING_TIMES_TARGETS_TXT) $(PARSING_VALIDATING_TIMES_TARGETS_TXT) validating_times.gpscript
 107         gnuplot validating_times.gpscript
 108
 109 validating_times: parsing_validating_times_candidates.ps validating_times_candidates.ps
 110
 111 clean:
 112         rm -f stats_candidates*.{xml,html,txt} \
 113           $(PARSING_TIMES_TARGETS_TXT) \
 114           $(PARSING_VALIDATING_TIMES_TARGETS_TXT) \
 115           $(VALIDATING_TIMES_TARGETS_TXT)
 116