From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 2 Dec 2019 12:42:43 +0000 (+0100)
Subject: updated web site
X-Git-Tag: make_still_working~215
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cdb85e803cd6038352ec0a318285f96f42faf02d

updated web site

+ new preprint J2a
+ some improvements
---

diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index 76705a3f8..2f35c1365 100644
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -6,7 +6,8 @@ TAGS = www up-html up-css up-images up-download \
        install-jed install-bib install-2 install-1 install-coq \
        install-automath install-v install-matita \
 
-LDURL   = http://lambdadelta.info/
+# LDURL = http://lambdadelta.info/
+LDURL = http://helm.cs.unibo.it/lambdadelta/
 
 SITEDIR    = html
 ETCDIR     = etc
diff --git a/helm/www/lambdadelta/download/basic2a.pdf b/helm/www/lambdadelta/download/basic2a.pdf
deleted file mode 100644
index e47b376d9..000000000
Binary files a/helm/www/lambdadelta/download/basic2a.pdf and /dev/null differ
diff --git a/helm/www/lambdadelta/download/gda.pdf b/helm/www/lambdadelta/download/gda.pdf
deleted file mode 100644
index 3a08c3242..000000000
Binary files a/helm/www/lambdadelta/download/gda.pdf and /dev/null differ
diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib
index 9e51a6b9b..b5dc547dc 100644
--- a/helm/www/lambdadelta/download/lambdadelta.bib
+++ b/helm/www/lambdadelta/download/lambdadelta.bib
@@ -26,13 +26,13 @@
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@comment{lambdadeltaR2d,
+@misc{lambdadeltaJ2a,
    author="Ferruccio {Guidi}",
    title="{Two Formal Systems of the $\lambda\delta$ Family Revised}",
-   howpublished="CoRR identifier 1411.0154",
-   year="2014",
+   howpublished="Preprint",
+   year="2019",
    month="November",
-   note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+   note="CoRR identifier 1911.12749",
 }
 
 @misc{lambdadeltaV2b,
@@ -52,7 +52,8 @@
    institution="University of Bologna",
    address="Bologna, Italy",
    year="2015",
-   month="December"
+   month="December",
+   note="CoRR identifier 1411.0154"
 }
 
 @misc{lambdadeltaV2a,
@@ -99,7 +100,8 @@
    publisher="ACM",
    address="New York, NY, USA",
    year="2009",
-   month="November"
+   month="November",
+   note="CoRR identifier cs/0611040"
 }
 
 @incollection{lambdadeltaR1c,
diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt
index 9e51a6b9b..b5dc547dc 100644
--- a/helm/www/lambdadelta/download/lambdadelta.txt
+++ b/helm/www/lambdadelta/download/lambdadelta.txt
@@ -26,13 +26,13 @@
 
 % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@comment{lambdadeltaR2d,
+@misc{lambdadeltaJ2a,
    author="Ferruccio {Guidi}",
    title="{Two Formal Systems of the $\lambda\delta$ Family Revised}",
-   howpublished="CoRR identifier 1411.0154",
-   year="2014",
+   howpublished="Preprint",
+   year="2019",
    month="November",
-   note="Preprint (available at $<$\url{http://lambdadelta.info/}$>$)"
+   note="CoRR identifier 1911.12749",
 }
 
 @misc{lambdadeltaV2b,
@@ -52,7 +52,8 @@
    institution="University of Bologna",
    address="Bologna, Italy",
    year="2015",
-   month="December"
+   month="December",
+   note="CoRR identifier 1411.0154"
 }
 
 @misc{lambdadeltaV2a,
@@ -99,7 +100,8 @@
    publisher="ACM",
    address="New York, NY, USA",
    year="2009",
-   month="November"
+   month="November",
+   note="CoRR identifier cs/0611040"
 }
 
 @incollection{lambdadeltaR1c,
diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml
index d8f43a7c9..80ef0b0ab 100644
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -15,7 +15,7 @@
       <rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
       <notice class="alpha" notice="view"/>
       <rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
-      (revised <notice class="gamma" notice="2018-01"/>).
+      (revised <notice class="gamma" notice="2019-11"/>).
    </body>
 
    <subsection name="v3"><img logo="ld3"/>λδ version 3 (proposed)</subsection>
diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl
index 2fedd9675..703ceebb1 100644
--- a/helm/www/lambdadelta/web/home/documentation_2.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_2.tbl
@@ -1,27 +1,29 @@
 name "documentation_2"
 
 table {
-(*
    [ { name "ldJ2a" "<span class=\"emph alpha\">J2a.</span>" "" } {
      "F. Guidi:" +
-     @@("download/basic2a.pdf"
-     "The Formal System λδ Revised, Stage A: Extending the Applicability Condition") +
-     "(<span class=\"emph gamma\">2014-11</span>)." +
+     @("https://arxiv.org/abs/1911.12749"
+     "Two Formal Systems of the λδ Family Revised") +
+     "(<span class=\"emph gamma\">2019-11</span>)." +
      "Preprint." + (* Submitted to ACM ToCL. *)
      "CoRR identifier" +
-     @("http://arxiv.org/abs/1411.0154" "1411.0154") +
-     "[v2] (revised" +
-     "<span class=\"emph gamma\">2015-03</span>)." +
+     @("https://arxiv.org/abs/1911.12749" "1911.12749") +
+     "[v1] (revised" +
+     "<span class=\"emph gamma\">2019-11</span>)." +
      @@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-*)
    [ { name "ldR2c" "<span class=\"emph alpha\">R2c.</span>" "" } {
      "F. Guidi:" + 
      @("http://amsacta.unibo.it/4411/"
      "Extending the Applicability Condition in the Formal System λδ") +
      "(<span class=\"emph gamma\">2015-03</span>)." +
      "University of Bologna, technical report AMS Acta 4411." +
+     "CoRR identifier" +
+     @("http://arxiv.org/abs/1411.0154" "1411.0154") +
+     "[v3] (revised" +
+     "<span class=\"emph delta\">2019-11</span>)." +
      @@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml
index e773b460b..92cd421bd 100644
--- a/helm/www/lambdadelta/web/home/home.ldw.xml
+++ b/helm/www/lambdadelta/web/home/home.ldw.xml
@@ -19,8 +19,14 @@
    <body>
       The λδ family is developed within the
       <link to="http://helm.cs.unibo.it/">Hypertextual Electronic Library of Mathematics (HELM)</link>
-      as a set of machine-checked digital specifications.
+      as a set of machine-checked <rlink to="html/specification.html">digital specifications</rlink>.
    </body>
+   <topitem name="current">
+      Current version:
+      <rlink to="download/lambdadelta_2B.tar.bz2">λδ-2B for for Matita 0.99.4</rlink>
+      (released: <notice class="gamma" notice="2019-11"/>).
+      <rlink to="html/documentation.html#ldJ2a">Documentation (J2a)</rlink>.
+   </topitem>
    <body>
       This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
       (revised <notice class="alpha" text="2012-09"/>).
@@ -171,5 +177,14 @@
       <link to="https://it.wikipedia.org/wiki/Umineko_no_naku_koro_ni">Umineko no Naku Koro ni</link>.
    </body>
 
+<!-- ===================================================================== -->
+
+   <section15 name="info">lambdadelta.info</section15>
+
+   <body>
+      <img logo="forward"/>
+      If this image is not visible, forwarding is out of order.
+   </body>
+
    <footer/>
 </page>
diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index 3a2740198..0dfec650c 100644
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -85,7 +85,7 @@
          <rlink to="download/lambdadelta_2B.tar.bz2">lambdadelta_2B for Matita 0.99.4</rlink>
          (revised <notice class="gamma" text="2019-11"/>).
          Source scripts [Git revision: 2019-11-19 20:45:15].
-         <rlink to="html/documentation.html#ldV2b">Documentation (V2b)</rlink>.
+         <rlink to="html/documentation.html#ldJ2a">Documentation (J2a)</rlink>.
       </body>
    </topitem>
 
diff --git a/helm/www/lambdadelta/xslt/ld_web_library.xsl b/helm/www/lambdadelta/xslt/ld_web_library.xsl
index e6b8df546..60b060249 100644
--- a/helm/www/lambdadelta/xslt/ld_web_library.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_library.xsl
@@ -88,8 +88,16 @@
 
 <!-- logo support -->
 
+<xsl:template name="forward-logo">
+   <a href="http://lambdadelta.info/"><img class="icon32"
+      alt="[forwarded logo]"
+      title="forwarded logo"
+      src="http://lambdadelta.info/images/crux_32.png"
+   /></a>
+</xsl:template>
+
 <xsl:template name="crux-logo">
-   <a href="{$baseurl}"><img class="icon32"
+   <a href="{$baseurl}html/home.html"><img class="icon32"
       alt="[\lambda\delta home]"
       title="\lambda\delta home"
       src="{$baseurl}images/crux_32.png"
@@ -150,6 +158,9 @@
 
 <xsl:template name="img">
   <xsl:choose>
+    <xsl:when test="@logo='forward'">
+      <xsl:call-template name="forward-logo"/>
+    </xsl:when>
     <xsl:when test="@logo='crux'">
       <xsl:call-template name="crux-logo"/>
     </xsl:when>