commit by user andrea

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

diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile
index e5a20a1f3212c7bf9cf6b4725d88eb7ce6f67242..3ce097690f439e6faa40dcd3c5cf3026a3bae0a4 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Makefile
+++ b/matita/matita/contribs/lambda_delta/Makefile
@@ -5,7 +5,7 @@ XOA     = xoa.native
 CONF    = Ground_2/xoa.conf.xml
 TARGETS = Ground_2/xoa_natation.ma Ground_2/xoa.ma
 
-PACKAGES = Ground_2 Basic_2
+PACKAGES = Ground_2 Basic_2 Apps_2
 
 all:
 
@@ -25,10 +25,12 @@ stats: $(PACKAGES:%=%.stats)
 
 %.stats: CHARS = $(shell cat $(MAS) | wc -c)
 
-%.stats: C1 = $(shell grep "inductive\|record" $(MAS) | wc -l)
-%.stats: C2 = $(shell grep "definition\|let rec" $(MAS) | wc -l)
+%.stats: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l)
+%.stats: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l)
+%.stats: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l)
 %.stats: P1 = $(shell grep "theorem " $(MAS) | wc -l)
 %.stats: P2 = $(shell grep "lemma " $(MAS) | wc -l)
+%.stats: P3 = $(shell grep "lemma \|theorem " $(MAS) | wc -l)
 
 %.stats: TBL = ld_$*_sum
 
@@ -65,20 +67,22 @@ stats: $(PACKAGES:%=%.stats)
        @printf '   %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
        @printf '   %-10s' ''
        @printf '\x1B[0m\n'
-       @printf 'name "$(TBL)"\n\n'                    > $*/$(TBL).tbl
-       @printf 'table {\n'                           >> $*/$(TBL).tbl
-       @printf '   class "grey" [ "category"\n'      >> $*/$(TBL).tbl
-       @printf '      [ "objects" * ]\n'             >> $*/$(TBL).tbl
-       @printf '   ]\n'                              >> $*/$(TBL).tbl
-       @printf '   class "green" [ "propositions"\n' >> $*/$(TBL).tbl
-       @printf '      [ "theorems" "$(P1)" * ]\n'    >> $*/$(TBL).tbl
-       @printf '      [ "lemmas"   "$(P2)" * ]\n'    >> $*/$(TBL).tbl
-       @printf '   ]\n'                              >> $*/$(TBL).tbl
-       @printf '   class "yellow" [ "concepts"\n'    >> $*/$(TBL).tbl
-       @printf '      [ "declared" "$(C1)" * ]\n'    >> $*/$(TBL).tbl
-       @printf '      [ "defined"  "$(C2)" * ]\n'    >> $*/$(TBL).tbl
-       @printf '   ]\n'                              >> $*/$(TBL).tbl
-       @printf '}\n\n'                               >> $*/$(TBL).tbl
-       @printf 'class "component" { 0 }\n\n'         >> $*/$(TBL).tbl
-       @printf 'class "plane" { 1 } { 3 } \n\n'      >> $*/$(TBL).tbl
-       @printf 'class "number" { 2 } { 4 } \n\n'     >> $*/$(TBL).tbl
+       @printf 'name "$(TBL)"\n\n'                      > $*/$(TBL).tbl
+       @printf 'table {\n'                             >> $*/$(TBL).tbl
+       @printf '   class "grey" [ "category"\n'        >> $*/$(TBL).tbl
+       @printf '      [ "objects" * ]\n'               >> $*/$(TBL).tbl
+       @printf '   ]\n'                                >> $*/$(TBL).tbl
+       @printf '   class "green" [ "propositions"\n'   >> $*/$(TBL).tbl
+       @printf '      [ "theorems" "$(P1)" * ]\n'      >> $*/$(TBL).tbl
+       @printf '      [ "lemmas"   "$(P2)" * ]\n'      >> $*/$(TBL).tbl
+       @printf '      [ "total"    "$(P3)" * ]\n'      >> $*/$(TBL).tbl
+       @printf '   ]\n'                                >> $*/$(TBL).tbl
+       @printf '   class "yellow" [ "concepts"\n'      >> $*/$(TBL).tbl
+       @printf '      [ "declared" "$(C1)" * ]\n'      >> $*/$(TBL).tbl
+       @printf '      [ "defined"  "$(C2)" * ]\n'      >> $*/$(TBL).tbl
+       @printf '      [ "total"    "$(C3)" * ]\n'      >> $*/$(TBL).tbl
+       @printf '   ]\n'                                >> $*/$(TBL).tbl
+       @printf '}\n\n'                                 >> $*/$(TBL).tbl
+       @printf 'class "component" { 0 }\n\n'           >> $*/$(TBL).tbl
+       @printf 'class "plane" { 1 } { 3 } { 5 } \n\n'  >> $*/$(TBL).tbl
+       @printf 'class "number" { 2 } { 4 } { 6 } \n\n' >> $*/$(TBL).tbl