- probe: new application to compute some data on the proof objects of

[helm.git] / matita / matita / contribs / lambdadelta / Makefile

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 7e267a2f31c6157d713f2c726ea6017ebd790f20..5b8fd2863b0b85461342da9b85b3e19b99f79be4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -1,3 +1,5 @@
+OPEN = (
+
 H        = @
 XOA_DIR  = ../../../components/binaries/xoa
 XOA      = xoa.native
@@ -5,6 +7,9 @@ DEP_DIR  = ../../../components/binaries/matitadep
 DEP      = matitadep.native
 MAC_DIR  = ../../../components/binaries/mac
 MAC      = mac.native
+PRB_DIR  = ../../../components/binaries/probe
+PRB      = probe.native
+PRB_OPTS = ../../matita.conf.xml -g cic:/matita/lambdadelta/
 
 XOA_CONF    = ground_2/xoa.conf.xml
 XOA_TARGETS = ground_2/xoa_notation.ma ground_2/xoa.ma
@@ -16,6 +21,16 @@ ORIGS    = basic_2/basic_1.orig
 PACKAGES = ground_2 basic_2 apps_2
 
 all:
+       ../../matitac.opt
+
+# MAS ########################################################################
+
+define MAS_TEMPLATE
+  MAS_$(1) := $$(shell find $(1) -name "*.ma")
+  MAS      += $$(MAS_$(1))
+endef
+
+$(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG))))
 
 # xoa ########################################################################
 
@@ -33,63 +48,77 @@ orig: $(ORIGS)
 
 # dep ########################################################################
 
-deps: MAS = $(shell find $* -name "*.ma")
-
 deps: $(DEP_DIR)/$(DEP)
        @echo "  MATITADEP"
        $(H)grep "include \"" $(MAS) | $<
 
 # stats ######################################################################
 
-stats: $(PACKAGES:%=%.stats)
-
-%.stats: MAS = $(shell find $* -name "*.ma")
-
-%.stats: CHARS = $(shell $(MAC_DIR)/$(MAC) $(MAS))
-
-%.stats:
+define STATS_TEMPLATE
+  STT_$(1) := $(1).stats
+  STTS     += $$(STT_$(1))
+
+  $$(STT_$(1)): S1 = $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1)))
+  $$(STT_$(1)): S2 := $$(shell echo $$$$(($$(S1) / 5120)))
+  $$(STT_$(1)): S4 := $$(shell ls $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): S5 := $$(shell $$(PRB_DIR)/$$(PRB) $$(PRB_OPTS)$(1)/ -sn -on)  
+  $$(STT_$(1)): P1 := $$(shell grep "theorem " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): P2 := $$(shell grep "lemma " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): P3 := $$(shell grep "fact " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): P4 := $$(shell grep qed $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): C1 := $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): C2 := $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): M1 := $$(shell grep "axiom " $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): M2 := $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l)
+  $$(STT_$(1)): M3 := $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l)
+
+$$(STT_$(1)):
        @printf '\x1B[1;40;37m'
-       @printf '%-15s %-40s' 'Statistics for:' $*      
-       @printf '\x1B[0m\n'     
+       @printf '%-15s %-43s' 'Statistics for:' $(1)
+       @printf '\x1B[0m\n'
        @printf '\x1B[1;40;35m'
-       @printf '%-8s %6i' Chars $(CHARS)
-       @printf '   %-8s %3i' Pages `echo $$(($(CHARS) / 5120))`
-       @printf '   %-23s' ''
+       @printf '%-8s %6i' Chars $$(S1)
+       @printf '   %-8s %3i' Pages $$(S2)
+       @printf '   %-26s' ''
        @printf '\x1B[0m\n'
        @printf '\x1B[1;40;36m'
-       @printf '%-8s %6i' Sources `ls $(MAS) | wc -l`
-       @printf '   %-38s' ''
-#      @printf '   %-8s %5i' Objs `ls *.vo | wc -l`
-#      @printf '   %-6s %3i' Files `ls *.v | wc -l`
+       @printf '%-8s %6i' Files $$(S4)
+       @printf '   %-8s %3i' Sources $$(word 1, $$(S5))        
+       @printf '   %-7s %4i' Objects $$(word 2, $$(S5))
+       @printf '   %-11s' ''
        @printf '\x1B[0m\n'     
        @printf '\x1B[1;40;32m'
-       @printf '%-8s %6i' Theorems `grep "theorem " $(MAS) | wc -l`
-       @printf '   %-8s %3i' Lemmas `grep "lemma " $(MAS) | wc -l`
-       @printf '   %-5s %3i' Facts `grep "fact " $(MAS) | wc -l`
-       @printf '   %-6s %4i' Proofs `grep qed $(MAS) | wc -l`
+       @printf '%-8s %6i' Theorems $$(P1)
+       @printf '   %-8s %3i' Lemmas $$(P2)
+       @printf '   %-7s %4i' Facts $$(P3)
+       @printf '   %-6s %4i' Proofs $$(P4)
        @printf '\x1B[0m\n'     
        @printf '\x1B[1;40;33m'
-       @printf '%-8s %6i' Declared `grep "inductive \|record " $(MAS) | wc -l` 
-       @printf '   %-8s %3i' Defined `grep "definition \|let rec " $(MAS) | wc -l`     
-       @printf '   %-23s' ''
-#      @printf '   %-8s %5i' Local `grep "Local" *.v | wc -l`
+       @printf '%-8s %6i' Declared $$(C1)
+       @printf '   %-8s %3i' Defined $$(C2)    
+       @printf '   %-26s' ''
        @printf '\x1B[0m\n'
        @printf '\x1B[1;40;31m'
-       @printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l`
-       @printf '   %-8s %3i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l`
-       @printf '   %-5s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
+       @printf '%-8s %6i' Axioms $$(M1)
+       @printf '   %-8s %3i' Comments $$(M2)
+       @printf '   %-7s %4i' Marks $$(M3)
        @printf '   %-11s' ''
        @printf '\x1B[0m\n'
+endef
+
+$(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG))))
+
+stats: $(STTS)
 
 # summary ####################################################################
 
 define SUMMARY_TEMPLATE
   TBL_$(1) := $(1)/$(1)_sum.tbl  
-  MAS_$(1) := $$(shell find $(1) -name "*.ma")
   TBLS     += $$(TBL_$(1))
 
-  $$(TBL_$(1)): V1 := $$(shell ls $$(MAS_$(1)) | wc -l)
-  $$(TBL_$(1)): V2 := $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1)))
+  $$(TBL_$(1)): S1 := $$(shell ls $$(MAS_$(1)) | wc -l)
+  $$(TBL_$(1)): S2 := $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1)))
+  $$(TBL_$(1)): S3 := $$(shell $$(PRB_DIR)/$$(PRB) $$(PRB_OPTS)$(1)/ -i)
   $$(TBL_$(1)): C1 := $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l)
   $$(TBL_$(1)): C2 := $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l)
   $$(TBL_$(1)): C3 := $$(shell grep "inductive \|record \|definition \|let rec " $$(MAS_$(1)) | wc -l)
@@ -105,9 +134,9 @@ define SUMMARY_TEMPLATE
        @printf '      [ "objects" * ]\n'              >> $$@
        @printf '   ]\n'                               >> $$@
        @printf '   class "cyan" [ "sizes"\n'          >> $$@
-       @printf '      [ "files" "$$(V1)" ]\n'         >> $$@
-       @printf '      [ "characters" "$$(V2)" ]\n'    >> $$@
-       @printf '      [ * ]\n'                        >> $$@
+       @printf '      [ "files" "$$(S1)" ]\n'         >> $$@
+       @printf '      [ "characters" "$$(S2)" ]\n'    >> $$@
+       @printf '      [ "nodes" "$$(S3)" ]\n'         >> $$@
        @printf '   ]\n'                               >> $$@   
        @printf '   class "green" [ "propositions"\n'  >> $$@
        @printf '      [ "theorems" "$$(P1)" ]\n'      >> $$@