]> matita.cs.unibo.it Git - helm.git/commitdiff
updated web site
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 2 Dec 2019 12:42:43 +0000 (13:42 +0100)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 2 Dec 2019 12:42:43 +0000 (13:42 +0100)
+ new preprint J2a
+ some improvements

helm/www/lambdadelta/Makefile
helm/www/lambdadelta/download/basic2a.pdf [deleted file]
helm/www/lambdadelta/download/gda.pdf [deleted file]
helm/www/lambdadelta/download/lambdadelta.bib
helm/www/lambdadelta/download/lambdadelta.txt
helm/www/lambdadelta/web/home/documentation.ldw.xml
helm/www/lambdadelta/web/home/documentation_2.tbl
helm/www/lambdadelta/web/home/home.ldw.xml
helm/www/lambdadelta/web/home/specification.ldw.xml
helm/www/lambdadelta/xslt/ld_web_library.xsl

index 76705a3f88c2fe0330d3f97a9e3cf3164f219343..2f35c136573f74114dd25b5ae9ebc506003ef97d 100644 (file)
@@ -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 (file)
index e47b376..0000000
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 (file)
index 3a08c32..0000000
Binary files a/helm/www/lambdadelta/download/gda.pdf and /dev/null differ
index 9e51a6b9b8a157e94fa3aa787b072ea512f0e362..b5dc547dcf7d4133f253be07e3d1ff9c850242f6 100644 (file)
 
 % \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,
    publisher="ACM",
    address="New York, NY, USA",
    year="2009",
-   month="November"
+   month="November",
+   note="CoRR identifier cs/0611040"
 }
 
 @incollection{lambdadeltaR1c,
index 9e51a6b9b8a157e94fa3aa787b072ea512f0e362..b5dc547dcf7d4133f253be07e3d1ff9c850242f6 100644 (file)
 
 % \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,
    publisher="ACM",
    address="New York, NY, USA",
    year="2009",
-   month="November"
+   month="November",
+   note="CoRR identifier cs/0611040"
 }
 
 @incollection{lambdadeltaR1c,
index d8f43a7c9be0b6446408e198035059a514653b8e..80ef0b0ab2f1aef5915dc16669656b1d6faa2ab5 100644 (file)
@@ -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>
index 2fedd967572ba93fded847f255cc322fb07c3026..703ceebb1c322a52a0b0928c236fd91d84a32e71 100644 (file)
@@ -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") ^ "."
      * }
    ]
index e773b460be5019d60319b3ea60b2616c14be0c21..92cd421bdb11f89c6ef7c523fc03bb0c6a275908 100644 (file)
    <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"/>).
       <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>
index 3a2740198f2af90ab8fab741cb0036d1bc3f0272..0dfec650c6e1bfe54109bdba52b2161212c2d8c7 100644 (file)
@@ -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>
 
index e6b8df546d02b66cb978351787722cf7d74d44eb..60b0602495b5e5b5e5222600e66abaa38ae05e25 100644 (file)
 
 <!-- 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"
 
 <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>