-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)):