X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2FMakefile;h=5b8fd2863b0b85461342da9b85b3e19b99f79be4;hb=06fae7628917399b6ceabace25607d6aafab0040;hp=38f1c3076fcc47ad8eb82c7d9c3e4dd0724724ca;hpb=380ceb6b6552fd9ebd48d710ab12931d5d97e465;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 38f1c3076..5b8fd2863 100644
--- 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
@@ -18,6 +23,15 @@ 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 ########################################################################
 
 xoa: $(XOA_TARGETS)
@@ -34,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)
@@ -106,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'      >> $$@