From: Ferruccio Guidi Date: Wed, 20 Nov 2019 18:08:07 +0000 (+0100) Subject: web site update X-Git-Tag: make_still_working~217 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=dd731f05f181f45260a0c448cf995aa3d7adc1f2 web site update + λδ-2B is released on web site + minor corrections --- diff --git a/helm/coq-contribs/lambdadelta/web/basic_1.ldw.xml b/helm/coq-contribs/lambdadelta/web/basic_1.ldw.xml new file mode 100644 index 000000000..d54d03e29 --- /dev/null +++ b/helm/coq-contribs/lambdadelta/web/basic_1.ldw.xml @@ -0,0 +1,49 @@ + + + + + + Abstract Syntax and Behavior + This is a summary of available syntactic items and reductions (block structure). + + + * In terms only. + + + Summary of the Specification + Here is a numerical account of the specification's contents + and its timeline. + +
+ + + λδ-1A is repackaged (was λδ-1). + + + λδ-1A is updated with backports from the abandoned specification of λδ-2. + + + λδ-1A is concluded. + + + Decidability of native type assignment, λδ-1A is released. + + + Preservation of native type by reduction, λδ-1A is announced. + + + λδ-1 started. + + + Logical Structure of the Specification + This table reports the specification's components and their planes. + +
+ +
+ diff --git a/helm/coq-contribs/lambdadelta/web/basic_1_blk.tbl b/helm/coq-contribs/lambdadelta/web/basic_1_blk.tbl new file mode 100644 index 000000000..996e35b50 --- /dev/null +++ b/helm/coq-contribs/lambdadelta/web/basic_1_blk.tbl @@ -0,0 +1,39 @@ +name "basic_1_blk" + +table { + class "gray" [ { "domain" * } { + [ + [ "block" ] [ "leader" ] + [ "→ζ *" ] [ "annotator (with →ϵ *)" ] + [ "applicator (with →θ *)" ] [ "reference *" ] [ "reduction" ] + ] + } ] + [ { "{X | Γ ⊢ ⊤}" * } { + class "wine" [ + [ "exclusion" ] [ "Γ ⊢ χ" ] + [ "yes" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] + [ { "{X | Γ ⊢ X : W}" * } { + class "magenta" [ + [ "typed abstraction" ] [ "Γ ⊢ λW" ] + [ "no" ] [ "<W>" ] [ "(V)" ] [ "#i" ] [ "→β *" ] + ] + } ] + [ { "{X | Γ ⊢ X = V}" * } { + class "prune" [ + [ "abbreviation" ] [ "Γ ⊢ δV" ] + [ "yes" ] [ "no" ] [ "no" ] [ "#i" ] [ "→δ" ] + ] + } ] + [ { "no" * } { + class "blue" [ + [ "sort" ] [ "Γ ⊢ ⋆k" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] +} + +class "top" { * } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta/web/basic_1_src.tbl b/helm/coq-contribs/lambdadelta/web/basic_1_src.tbl new file mode 100644 index 000000000..6afa13d55 --- /dev/null +++ b/helm/coq-contribs/lambdadelta/web/basic_1_src.tbl @@ -0,0 +1,218 @@ +name "basic_1_src" + +table uri "static/coq/lambdadelta/basic_1/" ext ".txt" { + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "wine" + [ { "examples" * } { + [ { "terms with special features" * } { + [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ] + } + ] + } + ] + class "magenta" + [ { "" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] +(* + [ { "higher order dynamic typing" * } { + [ { "higher order native type assignment" * } { + [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] + } + ] + } + ] +*) + class "prune" + [ { "dynamic typing" * } { + [ { "well-formed contexts" * } { + [ @@"wf3_defs" @@"wf3_props" * ] + } + ] + [ { "context ref. for native type assignment" * } { + [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ] + } + ] + [ { "native type assignment" * } { + [ @@"ty3_defs" @@"ty3_props" + @@"ty3_gen" + @@"ty3_gen_context" + @@"ty3_gen_nf2" + @@"ty3_lift" + @@"ty3_subst0" + @@"ty3_arity_props" + @@"ty3_nf2_gen" + @@"ty3_sred" + @@"ty3_sred_props" + @@"ty3_dec" * ] + } + ] + } + ] + class "blue" + [ { "equivalence" * } { + [ { "context-sensitive equivalence" * } { + [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ] + } + ] + [ { "context-free equivalence" * } { + [ @@"pc1_defs" @@"pc1_props" * ] + } + ] + } + ] + class "sky" + [ { "" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] + class "cyan" + [ { "computation" * } { + [ { "context ref. for reducibility" * } { + [ @@"csubc_defs" @@"csubc_props" * ] + } + ] + [ { "reducibility" * } { + [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ] + } + ] + [ { "strongly normalizing computation" * } { + [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ] + } + ] + [ { "context-sensitive computation" * } { + [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ] + } + ] + [ { "context-free computation" * } { + [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ] + } + ] + } + ] + class "water" + [ { "reduction" * } { + [ { "normal forms for context-sensitive reduction" * } { + [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ] + } + ] + [ { "context-sensitive reduction" * } { + [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ] + } + ] + [ { "normal forms for context-free reduction" * } { + [ "" @@"nf0_dec" * ] + } + ] + [ { "context-free reduction" * } { + [ @@"wcpr0_defs" * ] + [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ] + } + ] + } + ] + class "green" + [ { "unfold" * } { + [ { "iterated static type assignment" * } { + [ @@"sty1_defs" @@"sty1_props" * ] + } + ] + } + ] + class "grass" + [ { "static typing" * } { + [ { "static type assignment" * } { + [ @@"sty0_defs" @@"sty0_props" * ] + } + ] + [ { "context ref. for binary arity assignment" * } { + [ @@"csuba_defs" @@"csuba_props" * ] + } + ] + [ { "binary arity assignment" * } { + [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ] + } + ] + [ { "binary arity" * } { + [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ] + } + ] + [ { "parameters" * } { + [ @@"parameter_defs" * ] + } + ] + [ { "basic context ref." * } { + [ @@"csubv_defs" * ] + } + ] + } + ] + class "yellow" + [ { "multiple substitution" * } { + [ { "iterated context slicing" * } { + [ @@"drop1_defs" @@"drop1_props" * ] + } + ] + [ { "generic term relocation" * } { + [ @@"lift1_defs" @@"lift1_props" * ] + } + ] + } + ] + class "orange" + [ { "substitution" * } { + [ { "ordinary substitution" * } { + [ @@"subst_defs" @@"subst_props" * ] + [ @@"csubst1_defs" @@"csubst1_props" * ] + [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ] + } + ] + [ { "normal forms for ordinary strict substitution" * } { + [ "" @@"dnf_dec" * ] + } + ] + [ { "ordinary strict substitution" * } { + [ @@"fsubst0_defs" * ] + [ @@"csubst0_defs" * ] + [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ] + } + ] + [ { "basic local env. slicing" * } { + [ @@"getl_defs" @@"getl_props" * ] + [ @@"drop_defs" @@"drop_props" * ] + } + ] + [ { "basic term relocation" * } { + [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ] + } + ] + } + ] + class "red" + [ { "grammar" * } { + [ { "closures" * } { + [ @@"flt_defs" * ] + } + ] + [ { "contexts" * } { + [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ] + } + ] + [ { "terms" * } { + [ @@"tlist_defs" * ] + [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ] + } + ] + } + ] +} + +class "top" { * } + +class "capitalize italic" { 0 } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta/web/basic_1_sum.tbl b/helm/coq-contribs/lambdadelta/web/basic_1_sum.tbl new file mode 100644 index 000000000..717a4600a --- /dev/null +++ b/helm/coq-contribs/lambdadelta/web/basic_1_sum.tbl @@ -0,0 +1,28 @@ +name "basic_1_sum" + +table { + class "gray" [ "category" + [ "objects" * ] + ] + class "water" [ "sizes" + [ "files" "120" ] + [ "characters" "198089" ] + [ "nodes" "1449099" ] + ] + class "green" [ "propositions" + [ "theorems" "81" ] + [ "lemmas" "618" ] + [ "total" "699" ] + ] + class "grass" [ "concepts" + [ "declared" "39" ] + [ "defined" "47" ] + [ "total" "86" ] + ] +} + +class "capitalize italic" { 0 } + +class "italic" { 1 } { 3 } { 5 } + +class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/coq-contribs/lambdadelta/web/ground_1.ldw.xml b/helm/coq-contribs/lambdadelta/web/ground_1.ldw.xml new file mode 100644 index 000000000..846fe7ce9 --- /dev/null +++ b/helm/coq-contribs/lambdadelta/web/ground_1.ldw.xml @@ -0,0 +1,33 @@ + + + + + + Summary of the Specification + Here is a numerical account of the specification's contents + and its timeline. + +
+ + + Update with backports from the abandoned specification of λδ version 2. + + + Specification is concluded. + + + Specification starts. + + + Logical Structure of the Specification + This table reports the specification's components and their planes. + +
+ +
+ diff --git a/helm/coq-contribs/lambdadelta/web/ground_1_src.tbl b/helm/coq-contribs/lambdadelta/web/ground_1_src.tbl new file mode 100644 index 000000000..f8ce17263 --- /dev/null +++ b/helm/coq-contribs/lambdadelta/web/ground_1_src.tbl @@ -0,0 +1,50 @@ +name "ground_1_src" + +table uri "static/coq/lambdadelta/ground_1/" ext ".txt" { + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "grass" + [ { "multiple relocation" * } { + [ { "" * } { + [ @@"bg_plist" * ] + } + ] + } + ] + class "yellow" + [ { "extensions to the library" * } { + [ { "" * } { + [ @@"bg_hints" @@"bg_blt" * ] + } + ] + } + ] + class "orange" + [ { "generated logical decomposables" * } { + [ { "" * } { + [ @@"bg_types" @@"bg_props" * ] + } + ] + } + ] + class "red" + [ { "preamble" * } { + [ { "" * } { + [ @@"bg_require" @@"bg_rewrite" @@"bg_tactics" @@"bg_subst" * ] + } + ] + } + ] +} + +class "top" { * } + +class "capitalize italic" { 0 } + +class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta/web/ground_1_sum.tbl b/helm/coq-contribs/lambdadelta/web/ground_1_sum.tbl new file mode 100644 index 000000000..169c77b1a --- /dev/null +++ b/helm/coq-contribs/lambdadelta/web/ground_1_sum.tbl @@ -0,0 +1,28 @@ +name "ground_1_sum" + +table { + class "gray" [ "category" + [ "objects" * ] + ] + class "water" [ "sizes" + [ "files" "10" ] + [ "characters" "15063" ] + [ "nodes" "14881" ] + ] + class "green" [ "propositions" + [ "theorems" "0" ] + [ "lemmas" "50" ] + [ "total" "50" ] + ] + class "grass" [ "concepts" + [ "declared" "24" ] + [ "defined" "4" ] + [ "total" "28" ] + ] +} + +class "capitalize italic" { 0 } + +class "italic" { 1 } { 3 } { 5 } + +class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml b/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml deleted file mode 100644 index 421276cf2..000000000 --- a/helm/coq-contribs/lambdadelta_1/web/basic_1.ldw.xml +++ /dev/null @@ -1,46 +0,0 @@ - - - - - - Abstract Syntax and Behavior - This is a summary of available syntactic items and reductions (block structure). - -
- * In terms only. - - - Summary of the Specification - Here is a numerical account of the specification's contents - and its timeline. - -
- - - Update with backports from the abandoned specification of λδ version 2. - - - Specification is concluded. - - - Decidability of native type assignment, λδ version 1 is released. - - - Preservation of native type by reduction, λδ version 1 is announced. - - - Specification starts. - - - Logical Structure of the Specification - This table reports the specification's components and their planes. - -
- -
- diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl deleted file mode 100644 index 996e35b50..000000000 --- a/helm/coq-contribs/lambdadelta_1/web/basic_1_blk.tbl +++ /dev/null @@ -1,39 +0,0 @@ -name "basic_1_blk" - -table { - class "gray" [ { "domain" * } { - [ - [ "block" ] [ "leader" ] - [ "→ζ *" ] [ "annotator (with →ϵ *)" ] - [ "applicator (with →θ *)" ] [ "reference *" ] [ "reduction" ] - ] - } ] - [ { "{X | Γ ⊢ ⊤}" * } { - class "wine" [ - [ "exclusion" ] [ "Γ ⊢ χ" ] - [ "yes" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] - ] - } ] - [ { "{X | Γ ⊢ X : W}" * } { - class "magenta" [ - [ "typed abstraction" ] [ "Γ ⊢ λW" ] - [ "no" ] [ "<W>" ] [ "(V)" ] [ "#i" ] [ "→β *" ] - ] - } ] - [ { "{X | Γ ⊢ X = V}" * } { - class "prune" [ - [ "abbreviation" ] [ "Γ ⊢ δV" ] - [ "yes" ] [ "no" ] [ "no" ] [ "#i" ] [ "→δ" ] - ] - } ] - [ { "no" * } { - class "blue" [ - [ "sort" ] [ "Γ ⊢ ⋆k" ] - [ "no" ] [ "no" ] [ "no" ] [ "no" ] [ "no" ] - ] - } ] -} - -class "top" { * } - -class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl deleted file mode 100644 index 6afa13d55..000000000 --- a/helm/coq-contribs/lambdadelta_1/web/basic_1_src.tbl +++ /dev/null @@ -1,218 +0,0 @@ -name "basic_1_src" - -table uri "static/coq/lambdadelta/basic_1/" ext ".txt" { - class "gray" - [ { "component" * } { - [ { "plane" * } { - [ "files" * ] - } - ] - } - ] - class "wine" - [ { "examples" * } { - [ { "terms with special features" * } { - [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ] - } - ] - } - ] - class "magenta" - [ { "" * } { - [ { "" * } { - [ "" * ] - } - ] - } - ] -(* - [ { "higher order dynamic typing" * } { - [ { "higher order native type assignment" * } { - [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] - } - ] - } - ] -*) - class "prune" - [ { "dynamic typing" * } { - [ { "well-formed contexts" * } { - [ @@"wf3_defs" @@"wf3_props" * ] - } - ] - [ { "context ref. for native type assignment" * } { - [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ] - } - ] - [ { "native type assignment" * } { - [ @@"ty3_defs" @@"ty3_props" + @@"ty3_gen" + @@"ty3_gen_context" + @@"ty3_gen_nf2" + @@"ty3_lift" + @@"ty3_subst0" + @@"ty3_arity_props" + @@"ty3_nf2_gen" + @@"ty3_sred" + @@"ty3_sred_props" + @@"ty3_dec" * ] - } - ] - } - ] - class "blue" - [ { "equivalence" * } { - [ { "context-sensitive equivalence" * } { - [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ] - } - ] - [ { "context-free equivalence" * } { - [ @@"pc1_defs" @@"pc1_props" * ] - } - ] - } - ] - class "sky" - [ { "" * } { - [ { "" * } { - [ "" * ] - } - ] - } - ] - class "cyan" - [ { "computation" * } { - [ { "context ref. for reducibility" * } { - [ @@"csubc_defs" @@"csubc_props" * ] - } - ] - [ { "reducibility" * } { - [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ] - } - ] - [ { "strongly normalizing computation" * } { - [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ] - } - ] - [ { "context-sensitive computation" * } { - [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ] - } - ] - [ { "context-free computation" * } { - [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ] - } - ] - } - ] - class "water" - [ { "reduction" * } { - [ { "normal forms for context-sensitive reduction" * } { - [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ] - } - ] - [ { "context-sensitive reduction" * } { - [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ] - } - ] - [ { "normal forms for context-free reduction" * } { - [ "" @@"nf0_dec" * ] - } - ] - [ { "context-free reduction" * } { - [ @@"wcpr0_defs" * ] - [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ] - } - ] - } - ] - class "green" - [ { "unfold" * } { - [ { "iterated static type assignment" * } { - [ @@"sty1_defs" @@"sty1_props" * ] - } - ] - } - ] - class "grass" - [ { "static typing" * } { - [ { "static type assignment" * } { - [ @@"sty0_defs" @@"sty0_props" * ] - } - ] - [ { "context ref. for binary arity assignment" * } { - [ @@"csuba_defs" @@"csuba_props" * ] - } - ] - [ { "binary arity assignment" * } { - [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ] - } - ] - [ { "binary arity" * } { - [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ] - } - ] - [ { "parameters" * } { - [ @@"parameter_defs" * ] - } - ] - [ { "basic context ref." * } { - [ @@"csubv_defs" * ] - } - ] - } - ] - class "yellow" - [ { "multiple substitution" * } { - [ { "iterated context slicing" * } { - [ @@"drop1_defs" @@"drop1_props" * ] - } - ] - [ { "generic term relocation" * } { - [ @@"lift1_defs" @@"lift1_props" * ] - } - ] - } - ] - class "orange" - [ { "substitution" * } { - [ { "ordinary substitution" * } { - [ @@"subst_defs" @@"subst_props" * ] - [ @@"csubst1_defs" @@"csubst1_props" * ] - [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ] - } - ] - [ { "normal forms for ordinary strict substitution" * } { - [ "" @@"dnf_dec" * ] - } - ] - [ { "ordinary strict substitution" * } { - [ @@"fsubst0_defs" * ] - [ @@"csubst0_defs" * ] - [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ] - } - ] - [ { "basic local env. slicing" * } { - [ @@"getl_defs" @@"getl_props" * ] - [ @@"drop_defs" @@"drop_props" * ] - } - ] - [ { "basic term relocation" * } { - [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ] - } - ] - } - ] - class "red" - [ { "grammar" * } { - [ { "closures" * } { - [ @@"flt_defs" * ] - } - ] - [ { "contexts" * } { - [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ] - } - ] - [ { "terms" * } { - [ @@"tlist_defs" * ] - [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ] - } - ] - } - ] -} - -class "top" { * } - -class "capitalize italic" { 0 } - -class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl b/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl deleted file mode 100644 index 717a4600a..000000000 --- a/helm/coq-contribs/lambdadelta_1/web/basic_1_sum.tbl +++ /dev/null @@ -1,28 +0,0 @@ -name "basic_1_sum" - -table { - class "gray" [ "category" - [ "objects" * ] - ] - class "water" [ "sizes" - [ "files" "120" ] - [ "characters" "198089" ] - [ "nodes" "1449099" ] - ] - class "green" [ "propositions" - [ "theorems" "81" ] - [ "lemmas" "618" ] - [ "total" "699" ] - ] - class "grass" [ "concepts" - [ "declared" "39" ] - [ "defined" "47" ] - [ "total" "86" ] - ] -} - -class "capitalize italic" { 0 } - -class "italic" { 1 } { 3 } { 5 } - -class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml b/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml deleted file mode 100644 index 846fe7ce9..000000000 --- a/helm/coq-contribs/lambdadelta_1/web/ground_1.ldw.xml +++ /dev/null @@ -1,33 +0,0 @@ - - - - - - Summary of the Specification - Here is a numerical account of the specification's contents - and its timeline. - -
- - - Update with backports from the abandoned specification of λδ version 2. - - - Specification is concluded. - - - Specification starts. - - - Logical Structure of the Specification - This table reports the specification's components and their planes. - -
- -
- diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl b/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl deleted file mode 100644 index f8ce17263..000000000 --- a/helm/coq-contribs/lambdadelta_1/web/ground_1_src.tbl +++ /dev/null @@ -1,50 +0,0 @@ -name "ground_1_src" - -table uri "static/coq/lambdadelta/ground_1/" ext ".txt" { - class "gray" - [ { "component" * } { - [ { "plane" * } { - [ "files" * ] - } - ] - } - ] - class "grass" - [ { "multiple relocation" * } { - [ { "" * } { - [ @@"bg_plist" * ] - } - ] - } - ] - class "yellow" - [ { "extensions to the library" * } { - [ { "" * } { - [ @@"bg_hints" @@"bg_blt" * ] - } - ] - } - ] - class "orange" - [ { "generated logical decomposables" * } { - [ { "" * } { - [ @@"bg_types" @@"bg_props" * ] - } - ] - } - ] - class "red" - [ { "preamble" * } { - [ { "" * } { - [ @@"bg_require" @@"bg_rewrite" @@"bg_tactics" @@"bg_subst" * ] - } - ] - } - ] -} - -class "top" { * } - -class "capitalize italic" { 0 } - -class "italic" { 1 } diff --git a/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl b/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl deleted file mode 100644 index 169c77b1a..000000000 --- a/helm/coq-contribs/lambdadelta_1/web/ground_1_sum.tbl +++ /dev/null @@ -1,28 +0,0 @@ -name "ground_1_sum" - -table { - class "gray" [ "category" - [ "objects" * ] - ] - class "water" [ "sizes" - [ "files" "10" ] - [ "characters" "15063" ] - [ "nodes" "14881" ] - ] - class "green" [ "propositions" - [ "theorems" "0" ] - [ "lemmas" "50" ] - [ "total" "50" ] - ] - class "grass" [ "concepts" - [ "declared" "24" ] - [ "defined" "4" ] - [ "total" "28" ] - ] -} - -class "capitalize italic" { 0 } - -class "italic" { 1 } { 3 } { 5 } - -class "right italic" { 2 } { 4 } { 6 } diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index 6863484b7..9e51a6b9b 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -26,15 +26,24 @@ % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@comment{lambdadeltaJ2a, +@comment{lambdadeltaR2d, author="Ferruccio {Guidi}", - title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}", + title="{Two Formal Systems of the $\lambda\delta$ Family Revised}", howpublished="CoRR identifier 1411.0154", year="2014", month="November", note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)" } +@misc{lambdadeltaV2b, + author="Ferruccio {Guidi}", + title="{lambdadelta\_2B}", + howpublished="Formal specification for the interactive prover Matita 0.99.4", + year="2019", + month="November", + note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$" +} + @techreport{lambdadeltaR2c, author="Ferruccio {Guidi}", title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}", @@ -48,8 +57,8 @@ @misc{lambdadeltaV2a, author="Ferruccio {Guidi}", - title="{lambdadelta\_2A1}", - howpublished="Formal specification for the proof assistant Matita 0.99.2", + title="{lambdadelta\_2A}", + howpublished="Formal specification for the interactive prover Matita 0.99.2", year="2014", month="October", note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$" @@ -129,8 +138,8 @@ @misc{lambdadeltaV1a, author="Ferruccio {Guidi}", - title="{lambdadelta\_1}", - howpublished="Formal specification for the proof assistant Coq 7.3.1", + title="{lambdadelta\_1A}", + howpublished="Formal specification for the interactive prover Coq 7.3.1", year="2006", month="November", note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$" diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index 6863484b7..9e51a6b9b 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -26,15 +26,24 @@ % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@comment{lambdadeltaJ2a, +@comment{lambdadeltaR2d, author="Ferruccio {Guidi}", - title="{The Formal System $\lambda\delta$ Revised: Extending the Applicability Condition}", + title="{Two Formal Systems of the $\lambda\delta$ Family Revised}", howpublished="CoRR identifier 1411.0154", year="2014", month="November", note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)" } +@misc{lambdadeltaV2b, + author="Ferruccio {Guidi}", + title="{lambdadelta\_2B}", + howpublished="Formal specification for the interactive prover Matita 0.99.4", + year="2019", + month="November", + note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$" +} + @techreport{lambdadeltaR2c, author="Ferruccio {Guidi}", title="{Extending the Applicability Condition in the Formal System $\lambda\delta$}", @@ -48,8 +57,8 @@ @misc{lambdadeltaV2a, author="Ferruccio {Guidi}", - title="{lambdadelta\_2A1}", - howpublished="Formal specification for the proof assistant Matita 0.99.2", + title="{lambdadelta\_2A}", + howpublished="Formal specification for the interactive prover Matita 0.99.2", year="2014", month="October", note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$" @@ -129,8 +138,8 @@ @misc{lambdadeltaV1a, author="Ferruccio {Guidi}", - title="{lambdadelta\_1}", - howpublished="Formal specification for the proof assistant Coq 7.3.1", + title="{lambdadelta\_1A}", + howpublished="Formal specification for the interactive prover Coq 7.3.1", year="2006", month="November", note="Available at $\lambda\delta$ Web site: $<$\url{http://lambdadelta.info/}$>$" diff --git a/helm/www/lambdadelta/download/lambdadelta_1.tar.gz b/helm/www/lambdadelta/download/lambdadelta_1.tar.gz deleted file mode 100644 index 77c80d964..000000000 Binary files a/helm/www/lambdadelta/download/lambdadelta_1.tar.gz and /dev/null differ diff --git a/helm/www/lambdadelta/download/lambdadelta_1A.tar.bz2 b/helm/www/lambdadelta/download/lambdadelta_1A.tar.bz2 new file mode 100644 index 000000000..8792dd8f7 Binary files /dev/null and b/helm/www/lambdadelta/download/lambdadelta_1A.tar.bz2 differ diff --git a/helm/www/lambdadelta/download/lambdadelta_2A.tar.bz2 b/helm/www/lambdadelta/download/lambdadelta_2A.tar.bz2 new file mode 100644 index 000000000..d82582bbc Binary files /dev/null and b/helm/www/lambdadelta/download/lambdadelta_2A.tar.bz2 differ diff --git a/helm/www/lambdadelta/download/lambdadelta_2A1.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2A1.tar.gz deleted file mode 100644 index ff9bc8307..000000000 Binary files a/helm/www/lambdadelta/download/lambdadelta_2A1.tar.gz and /dev/null differ diff --git a/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 b/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 index 33786f969..4a4e63330 100644 Binary files a/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 and b/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 differ diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl index 2fe3ea0e6..e2b6c590c 100644 --- a/helm/www/lambdadelta/web/home/documentation_1.tbl +++ b/helm/www/lambdadelta/web/home/documentation_1.tbl @@ -88,8 +88,8 @@ table { ] [ { name "ldV1a" "V1a." "" } { "F. Guidi:" + - @@("html/version_1.html" "lambdadelta_1") + - "(revised 2015-01)." + + @@("html/version_1.html" "lambdadelta_1A") + + "(revised 2019-11)." + "Formal specification for the proof assistant Coq 7.3.1 (scripts)." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 2cd06743e..64ffcf1af 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -94,8 +94,8 @@ table { ] [ { name "ldV2a" "V2a." "" } { "F. Guidi:" + - @@("html/version_2.html" "lambdadelta_2A1") + - "(revised 2014-10)." + + @@("html/version_2.html" "lambdadelta_2A") + + "(revised 2019-11)." + "Formal specification for the proof assistant Matita 0.99.2 (scripts)." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." * } diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 27e6dd460..3538b68d9 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -12,12 +12,23 @@ Milestones + + The specifications of λδ-1A and λδ-2A are repackaged + (they were λδ-1 and λδ-2A1 respectively). + + The specification of - λδ-2B + λδ-2B is released. + + The specification of + λδ-2B + is announced. + + Second journal paper on λδ accepted for publication. @@ -27,6 +38,10 @@ "Helena 0.8.3" is released. + + The specification of λδ-2B is started. + + The specification of λδ-2A is concluded. @@ -64,7 +79,7 @@ The specification of - λδ-2A + λδ-2A is released. @@ -73,7 +88,9 @@ - First communication on λδ-2. + The specification of + λδ-2A + is announced. @@ -147,7 +164,7 @@ - The + The HTML pages of the specification of λδ-1A for Matita 0.5 are online. @@ -161,19 +178,21 @@ - The + The specification of λδ-1A for Matita 0.4 is online. The specification of - λδ-1A + λδ-1A is released. - First communication on λδ-1. + The specification of + λδ-1A + is announced. @@ -185,16 +204,16 @@ Visibility - + The Google search for "formal system lambda delta" gives - 5 resources about the λδ family in the first 6 results. + 9 resources about the λδ family in the first 10 results. - + The Yahoo search for "formal system lambda delta" gives - 4 resources about the λδ family in the first 5 results. + 14 resources about the λδ family in the first 14 results.
diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index c58b253a8..ecd3ffabf 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -58,27 +58,9 @@ λδ version 2 (active) The formal specification of λδ version 2 - is available in the following formats: + is available in the following formats. - - - lambdadelta_2A1 for Matita 0.99.2 - (revised ). - Source scripts [Svn revision: 12964]. - Documentation (R2c). - - - The scripts are grouped in directories, first by part, then by component. - - - - the scripts are checked by the latest version of Matita from - HELM Subversion repository - at path <trunk/matita/>. - - - Informational pages on the parts of the specification: Background, @@ -87,33 +69,77 @@ Applications. + + + The scripts are grouped in directories, first by part, then by component. + + + + + the scripts are checked by the latest version of Matita from + helm.git repository. + + + + + lambdadelta_2B for Matita 0.99.4 + (revised ). + Source scripts [Git revision: 2019-11-19 20:45:15]. + Documentation (V2b). + + + + + + lambdadelta_2A for Matita 0.99.2 + (revised ). + Source scripts [Git revision: 2014-10-28 17:46:26]. + Documentation (R2c). + + + repackaging (was lambdadelta_2A1). + + + + λδ version 1 (superseded) The formal specification of λδ version 1 - is available in the following formats: + is available in the following formats. - + + Informational pages on the parts of the specification: + Background, + Core. + + + + + The scripts are grouped in directories, one for each part. + + + - lambdadelta_1 for Coq 7.3.1 - (revised ). + lambdadelta_1A for Coq 7.3.1 + (revised ). Source scripts. Documentation (J1a). + + repackaging (was lambdadelta_1). + 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg". - - The scripts are grouped in directories, one for each part. - - - lambdadelta_1 for Matita 0.5 - (revised ). + + lambdadelta_1A for Matita 0.5 + (revised ). Static HTML pages generated by the HELM rendering engine. @@ -137,19 +163,13 @@ - + - lambdadelta_1 for Matita 0.5 - (revised ). + lambdadelta_1A for Matita 0.5 + (revised ). HELM directory. - - Informational pages on the parts of the specification: - Background, - Core. - -
diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index e22b7ec42..ff1ebeeef 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -261,7 +261,7 @@ trim: $(TRIMS:%=%.trimmed) contrib: @echo " TAR -cjf $(CONTRIB).tar.bz2 root $(XPACKAGES)" - $(H)tar -cjf $(CONTRIB).tar.bz2 root $(XMAS) + $(H)tar -cjf $(CONTRIB).tar.bz2 ../lambdadelta/root $(XMAS:%=../lambdadelta/%) # clean ###################################################################### diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 74e37e0da..e40771d8e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -101,6 +101,9 @@ Stage "A" + + λδ-2A is repackaged (was λδ-2A1). + λδ-2A appears too complex and is dismissed.