From: Ferruccio Guidi Date: Wed, 27 Nov 2013 21:47:16 +0000 (+0000) Subject: web page for ground_2 and bugfixed statistics generation in the Makefile X-Git-Tag: make_still_working~1043 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4cd0faedb102c866719990bc1e61b099db0ea39d;p=helm.git web page for ground_2 and bugfixed statistics generation in the Makefile --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 6eed87bc1..16c000e67 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -118,13 +118,13 @@ define STATS_TEMPLATE $$(STT_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) $$(STT_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt) $$(STT_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) - $$(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)): 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)): 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) @@ -180,12 +180,12 @@ define SUMMARY_TEMPLATE $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) $$(SUM_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt) $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): C1 = $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): C2 = $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): C3 = $$(shell grep "inductive \|record \|definition \|let rec " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): P1 = $$(shell grep "theorem " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): P2 = $$(shell grep "lemma " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): P3 = $$(shell grep "lemma \|theorem " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): C3 = $$(shell grep "^inductive \|^record \|^definition \|^let rec " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): P2 = $$(shell grep "^lemma " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): P3 = $$(shell grep "^lemma \|^theorem " $$(MAS_$(1)) | wc -l) $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt @printf ' SUMMARY $(1)\n' diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml new file mode 100644 index 000000000..f1ea686a1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml @@ -0,0 +1,38 @@ + + + +
Summary of the Specification
+ Here is a numerical acount of the specification's contents + and its timeline. + Nodes are counted according to the "intrinsinc complexity measure" + [F. Guidi: "Procedural Representation of CIC Proof Terms" + Journal of Automated Reasoning 44(1-2), Springer (February 2010), + pp. 53-78]. + + + + Natural numbers with infinity. + + + Specification starts. + + +
Logical Structure of the Specification
+ The source files are grouped in planes + according to the following table. + Notation files covering the whole specification are provided. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). + +
+ +
Physical Structure of the Specification
+ The source files are grouped in directories, + one for each plane. + +
+ diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl new file mode 100644 index 000000000..3eec66de3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -0,0 +1,23 @@ +name "ground_2_src" + +table { + class "grey" + [ { "plane" * } { + [ "files" * ] + } + ] + class "orange" + [ { "natural numbers with infinity" * } { + [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" * ] + } + ] + class "red" + [ { "" * } { + [ "" * ] + } + ] +} + +class "plane" { 0 } + +class "file" { 1 * }