From: Claudio Sacerdoti Coen
Date: Fri, 27 Sep 2019 14:52:38 +0000 (+0200)
Subject: Merge branch 'declarative' into matita-lablgtk3
X-Git-Tag: make_still_working~229^2~1^2~1
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=4112b9f87a555bfc4c3cd06bae652cd2382cad8b
Merge branch 'declarative' into matita-lablgtk3
---
diff --git a/.gitignore b/.gitignore
index 59fdc3df1..e7228e3ba 100644
--- a/.gitignore
+++ b/.gitignore
@@ -66,6 +66,7 @@ helm/www/lambdadelta/xslt/documentation_3.xsl
helm/www/lambdadelta/xslt/sitemap.xsl
helm/www/lambdadelta/xslt/versions.xsl
helm/www/lambdadelta/xslt/core.xsl
+helm/www/lambdadelta/xslt/changes.xsl
helm/www/lambdadelta/xslt/chc_45.xsl
helm/www/lambdadelta/xslt/xhtbl.xsl
@@ -75,3 +76,5 @@ matita/matita/contribs/lambdadelta/token
matita/matita/contribs/lambdadelta/2A
matita/matita/contribs/lambdadelta/*/*_probe.txt
matita/matita/contribs/lambdadelta/*/web/*_sum.tbl
+
+matita/matita/contribs/convergence/
diff --git a/README b/README
index 4aad3fc69..4d1a6c03b 100644
--- a/README
+++ b/README
@@ -1,3 +1,3 @@
-matita : current version: 0.99.3
+matita : current version: 0.99.4
matitaB: new version: 0.5.8
helm : old version: 0.5.8 with additional material
diff --git a/helm/www/lambdadelta/alt.sh b/helm/www/lambdadelta/alt.sh
new file mode 100644
index 000000000..80a326f64
--- /dev/null
+++ b/helm/www/lambdadelta/alt.sh
@@ -0,0 +1 @@
+sed s?lambdadelta.info?www.cs.unibo.it/~fguidi/lambdadelta?g html/$1.html > html/$1.alt.html
diff --git a/helm/www/lambdadelta/css/martha.css b/helm/www/lambdadelta/css/martha.css
index 68e956194..59c7c821a 100644
--- a/helm/www/lambdadelta/css/martha.css
+++ b/helm/www/lambdadelta/css/martha.css
@@ -1,23 +1,40 @@
@charset "UTF-8";
-/* menus ********************************************************************/
+/* term selection ***********************************************************/
-td {
- padding: inherit;
+.term:hover > .term:not(:hover) {
+ opacity: 0.35;
}
+/* log table ****************************************************************/
+
+.log {
+ width: 100%;
+ border-collapse: collapse;
+}
+
+.log_cell {
+ border-color: initial;
+ border-style: solid none;
+ border-width: thin;
+ padding: 2px;
+}
+
+/* forms ********************************************************************/
+
.text {
display: inline-block;
list-style: none;
margin: initial;
padding: initial;
- white-space: nowrap;
+ white-space: nowrap;
}
.menu {
display: none;
border-style: solid;
border-width: thin;
+ border-collapse: collapse;
position: absolute;
}
@@ -25,14 +42,34 @@ td {
display: inline-block;
}
+.menu_cell {
+ padding: 2px;
+}
+
+.menu_empty {
+ padding: inherit;
+}
+
+.menu_sep {
+ padding: inherit;
+ border-top-style: solid;
+ border-top-width: thin;
+}
+
/* buttons ******************************************************************/
+.type {
+ font: inherit;
+}
+
.button {
- color: inherit;
background-color: inherit;
- border-style: none;
+ border-style: none;
+ color: inherit;
+ font: inherit;
margin: initial;
padding: initial;
+ text-align: inherit;
}
.button:hover {
@@ -83,13 +120,13 @@ a:active {
/* font families ************************************************************/
.monospace {
- font-family:monospace;
+ font-family: monospace; "Courier New", Courier;
}
/* line heights *************************************************************/
.l_150 {
- line-height:150%;
+ line-height: 150%;
}
/* font sizes ***************************************************************/
@@ -100,21 +137,25 @@ a:active {
/* foreground colors (equalized to gray 8F) *********************************/
+.f_white {
+ color:#FFFFFF;
+}
+
.f_gray {
color:#8F8F8F;
}
.f_wine {
- color:#FF52A0;
-}
+ color:#FF52A0;
+}
.f_magenta {
- color:#FF41FF;
-}
+ color:#FF41FF;
+}
.f_prune {
- color:#C65DFF;
-}
+ color:#C65DFF;
+}
.f_blue {
color:#8181FF;
@@ -187,7 +228,7 @@ a:active {
}
.b_cyan {
- background-color:#6CFFFF;
+ background-color:#6CFFFF;
}
.b_water {
@@ -214,8 +255,30 @@ a:active {
background-color:#FFC0C0;
}
+.b_black {
+ background-color:#000000;
+}
+
/* background colors (equalized to gray EB) *********************************/
.b_gray_EB {
background-color:#EBEBEB;
}
+
+.b_blue_EB {
+ background-color:#E8E8FF;
+}
+
+.b_orange_EB {
+ background-color:#FFEBB1;
+}
+
+.b_red_EB {
+ background-color:#FFE2E2;
+}
+
+/* background colors (equalized to gray 48) *********************************/
+
+.b_gray_48 {
+ background-color:#484848;
+}
diff --git a/helm/www/lambdadelta/images/bronze-03BB.png b/helm/www/lambdadelta/images/bronze-03BB.png
new file mode 100644
index 000000000..3cf590000
Binary files /dev/null and b/helm/www/lambdadelta/images/bronze-03BB.png differ
diff --git a/helm/www/lambdadelta/web/home/changes.ldw.xml b/helm/www/lambdadelta/web/home/changes.ldw.xml
new file mode 100644
index 000000000..4287ac584
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/changes.ldw.xml
@@ -0,0 +1,17 @@
+
+
+
+
+
+ Changes
+
+
+
+
+
+
diff --git a/helm/www/lambdadelta/web/home/changes.tbl b/helm/www/lambdadelta/web/home/changes.tbl
new file mode 100644
index 000000000..d25be28c7
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/changes.tbl
@@ -0,0 +1,118 @@
+name "changes"
+
+table {
+ class "gray"
+ [ "version" [ "aspect" [ "" "changes" ]]
+ ]
+
+ class "orange"
+ [ { "λδ-2B" + "(unreleased)" * }
+ {
+ [ [{ "equivalences" * }]
+ { "+" "+" "+" "-" }
+ { "equivalence for full rt-reduction (terms)"
+ "equivalence for whd rt-reduction (terms)"
+ "equivalence for extended rt-reduction (terms, referred lenvs, closures)"
+ "syntactic equivalence (closures) removed"
+ }
+ ]
+ [ [{ "weights" * }]
+ { "+" }
+ { "switch in primitive order relations for closures to enable the exclusion binder"
+ }
+ ]
+ [ [{ "relocation" * }]
+ { "" }
+ { ""
+ }
+ ]
+ [ [{ "syntax" * }]
+ { "+" }
+ { "exclusion binder for lenvs"
+ }
+ ]
+ [ [{ "ground" * }]
+ { "+" "*" "+" "-" }
+ { "rt-transition counters"
+ "generic reference transforming maps as streams of non-negative integers"
+ "extensional equality, labelled transitive closures and streams"
+ "non-negative integers with infinity removed"
+ }
+ ]
+ }
+ ]
+
+ class "orange"
+ [ { "λδ-2A" + "(October 2014)" * }
+ {
+ [ [{ "equivalences" * }]
+ { "+" }
+ { "syntactic equivalence (selected lenvs, referred lenvs, closures)"
+ }
+ ]
+ [ [{ "weights" * }]
+ { "*" "-" }
+ { "primitive order relations for closures"
+ "complex weight (terms) removed"
+ }
+ ]
+ [ [{ "relocation" * }]
+ { "-" }
+ { "level update functions removed"
+ }
+ ]
+ [ [{ "syntax" * }]
+ { "+" "+" "+" "-" "-" }
+ { "polarized binders for terms"
+ "non-negative integer global references for terms"
+ "syntactic support for genvs with typed abstraction, abbreviation"
+ "numbered sorts, application, type annotation removed from lenvs"
+ "exclusion binder removed from terms and lenvs"
+ }
+ ]
+ [ [{ "ground" * }]
+ { "+" "+" }
+ { "lists and non-negative integers with infinity"
+ "library extension for transitive closures and booleans"
+ }
+ ]
+ }
+ ]
+
+ class "red"
+ [ { "λδ-1A" + "(November 2006)" * }
+ {
+ [ [{ "equivalences" * }]
+ { "" }
+ { "equivalence for outer reduction (terms)"
+ }
+ ]
+ [ [{ "weights" * }]
+ { "" "" "" }
+ { "order relations (terms, lenvs, closures) based on weights"
+ "simple weights (terms, lenvs, closures)"
+ "complex weight (terms)"
+ }
+ ]
+ [ [{ "relocation" * }]
+ { "" }
+ { "level update functions"
+ }
+ ]
+ [ [{ "syntax" * }]
+ { "" "" }
+ { "lenvs with non-negative integer sorts, application, typed abstraction, abbreviation, exclusion, type annotation"
+ "terms with non-negative integer sorts and local references, application, typed abstraction, abbreviation, exclusion, type annotation" }
+ ]
+ [ [{ "ground" * }]
+ { "" "" }
+ { "finite reference transforming maps as compositions of basic ones"
+ "library extension for logic and non-negative integers"
+ }
+ ]
+ }
+ ]
+
+}
+
+class "center" { 2 }
diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml
index 8e6135836..e773b460b 100644
--- a/helm/www/lambdadelta/web/home/home.ldw.xml
+++ b/helm/www/lambdadelta/web/home/home.ldw.xml
@@ -30,6 +30,9 @@
to view this site correctly, please select a font
with Unicode support.
+
+