- nUri : added Sets of uris for use in "probe"

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

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 5b8fd2863b0b85461342da9b85b3e19b99f79be4..f13eb7e21ff48573eac5b4197b5a89be96fd801c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -9,7 +9,7 @@ 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/
+PRB_OPTS = ../../matita.conf.xml -g
 
 XOA_CONF    = ground_2/xoa.conf.xml
 XOA_TARGETS = ground_2/xoa_notation.ma ground_2/xoa.ma
@@ -61,7 +61,7 @@ define STATS_TEMPLATE
   $$(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)): 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)
@@ -74,39 +74,41 @@ define STATS_TEMPLATE
 
 $$(STT_$(1)):
        @printf '\x1B[1;40;37m'
-       @printf '%-15s %-43s' 'Statistics for:' $(1)
+       @printf '%-15s %-44s' 'Statistics for:' $(1)
        @printf '\x1B[0m\n'
        @printf '\x1B[1;40;35m'
        @printf '%-8s %6i' Chars $$(S1)
-       @printf '   %-8s %3i' Pages $$(S2)
+       @printf '   %-8s %4i' Pages $$(S2)
        @printf '   %-26s' ''
        @printf '\x1B[0m\n'
        @printf '\x1B[1;40;36m'
        @printf '%-8s %6i' Files $$(S4)
-       @printf '   %-8s %3i' Sources $$(word 1, $$(S5))        
+       @printf '   %-8s %4i' 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 $$(P1)
-       @printf '   %-8s %3i' Lemmas $$(P2)
+       @printf '   %-8s %4i' 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 $$(C1)
-       @printf '   %-8s %3i' Defined $$(C2)    
+       @printf '   %-8s %4i' Defined $$(C2)    
        @printf '   %-26s' ''
        @printf '\x1B[0m\n'
        @printf '\x1B[1;40;31m'
        @printf '%-8s %6i' Axioms $$(M1)
-       @printf '   %-8s %3i' Comments $$(M2)
+       @printf '   %-8s %4i' Comments $$(M2)
        @printf '   %-7s %4i' Marks $$(M3)
        @printf '   %-11s' ''
        @printf '\x1B[0m\n'
 endef
 
-$(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG))))
+ifeq ($(MAKECMDGOALS), stats)
+   $(foreach PKG, $(PACKAGES), $(eval $(call STATS_TEMPLATE,$(PKG))))
+endif
 
 stats: $(STTS)
 
@@ -118,7 +120,7 @@ define SUMMARY_TEMPLATE
 
   $$(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)): 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)
@@ -154,6 +156,8 @@ define SUMMARY_TEMPLATE
        @printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $$@
 endef
 
-$(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG))))
+ifeq ($(MAKECMDGOALS), tbls)
+   $(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG))))
+endif
 
 tbls: $(TBLS)