lddl update with the disambiguated "grundlagen"

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index 07ecd4e4e30965c710018d13c851f956788c0096..e35c1c85adcb15f744fd3ab19a4099a0ef317f90 100644 (file)
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -10,7 +10,8 @@ KEEP = README
 
 CLEAN = etc/log.txt etc/profile.txt
 
-TAGS = test-si-fast test-si test-si-matita test profile xml xml-v3 matita matitac 
+TAGS = test-si-fast test-si test-si-matita test profile \
+       xml-si xml-si-v3 xml xml-v3 matita matitac 
 
 include Makefile.common
 
@@ -50,13 +51,21 @@ profile: $(MAIN).opt etc
        $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done
        $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt
 
+xml-si: $(MAIN).opt etc
+       @echo "  HELENA -l -o -s 1 -x $(INPUT)"
+       $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -x $(INPUT) > etc/log.txt
+
+xml-si-v3: $(MAIN).opt etc
+       @echo "  HELENA -l -o -s 2 -x $(INPUT)"
+       $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -x $(INPUT) > etc/log.txt
+
 xml: $(MAIN).opt etc
        @echo "  HELENA -l -s 1 -x $(INPUT)"
        $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 1 -x $(INPUT) > etc/log.txt
 
 xml-v3: $(MAIN).opt etc
        @echo "  HELENA -l -s 2 -x $(INPUT)"
-       $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 3 -x $(INPUT) > etc/log.txt
+       $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 2 -x $(INPUT) > etc/log.txt
 
 matita: matita/$(MA)
        @echo "  MATITA $(MA)"

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 3a394c5b7803191f47cddbafbdf98ac597b4147e..227a524e2036ca126238288d7e061b7f4bd1c649 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -55,10 +55,14 @@ let ma_preamble = ref ""     (* location of grafite preamble file *)
 
 let alpha = ref ""           (* prefix of numeric identifiers *)
 
-let kernel_id () = match !kernel with
-   | V4 -> ""
-   | V3 -> "V3"
-   | V0 -> "V0"
+let kernel_id () = 
+   let id = match !kernel with
+      | V4 -> "Environment"
+      | V3 -> "Environment_V3"
+      | V0 -> "Environment_V0"
+   in
+   let si = if !si then "_si" else "" in
+   id ^ si
 
 let get_baseuri () =
    String.concat "/" ["ld:"; kernel_id (); !cover; "" ]

diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml
index d51af0bfb742b66e32af98e90ab47baad0cc5edc..584dc776a7b8d4a0d533c1b69a1ebce7e2f01414 100644 (file)
--- a/helm/software/helena/src/xml/xmlLibrary.ml
+++ b/helm/software/helena/src/xml/xmlLibrary.ml
@@ -133,7 +133,8 @@ let export_entity pp_term (ra, na, u, b) =
       | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
       | E.Void   -> assert false
    in
+   let opts = if !G.si then "si" else "" in
    let shp = H.string_of_graph () in
-   let attrs = [xmlns; "hierarchy", shp] in
+   let attrs = [xmlns; "hierarchy", shp; "options", opts] in
    tag obj_root attrs ~contents out 0;
    close_out och

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 21925537541dc339c43ea1ebbfbf54bc38563f86..9050909b225b1cb6c211f003b53b1be2fa73c0cb 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -223,6 +223,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:52 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index c583563f0f480d68c698c82160a64a18b71004b3..b8b2996adbf1b86382316339c0832924cdc74876 100644 (file)
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -23,18 +23,20 @@ WEBDIRS  = $(SRCDIR) $(ETCDIR)
 
 REMOTE   = helm.cs.unibo.it
 RDIR     = /projects/helm/public_html/lambdadelta
-RXMLDIR  = $(REMOTE):$(RDIR)/xml
-RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl
+RHOMEDIR = $(REMOTE):$(RDIR)
+RXMLDIR  = $(RHOMEDIR)/xml
+RHTMLDIR = $(RHOMEDIR)/static/lddl
+RDOWNDIR = $(RHOMEDIR)/download
 
 SLS     = helena.sl automath.sl
 BIB     = lambdadelta.bib
 CONTRIB = lambdadelta_2.tar.gz
 
-XMLS = grundlagen_2/l/not.ld.xml \
-       grundlagen_2/l/et.ld.xml \
-       grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
-       grundlagen_2/l/e/pairis1.ld.xml \
-       grundlagen_2/l/e/st/eq/landau/n/327/t25.ld.xml \
+XMLS = Environment/grundlagen_2/l/not.ld.xml \
+       Environment/grundlagen_2/l/et.ld.xml \
+       Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+       Environment/grundlagen_2/l/e/pairis1.ld.xml \
+       Environment/grundlagen_2/l/e/st/eq/landau/n/327/t25.ld.xml \
 
 LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl
 
@@ -93,13 +95,16 @@ $(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index:
        $(H)find $(XMLDIR) -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > $(XMLDIR)/index.txt
        $(H)sed "s/^/make --no-print-directory /" $(XMLDIR)/index.txt | sed s.ld:/.. > $(ETCDIR)/make_html.sh
 
-lddl: $(ETCDIR)/exclude.txt index
+$(DOWNDIR)/lddl.tar.bz2 lddl: $(ETCDIR)/exclude.txt $(XMLDIR)/index.txt
        @echo "  GENERATE lddl.tar.bz2"
        $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR) 
 
-install-xml: $(XMLDIR)/index.txt
+install-xml: $(DOWNDIR)/lddl.tar.bz2 
        @echo "  INSTALL xml"
-       $(H)scp -r $< $(XMLDIR)/brg_si/ $(XMLDIR)/crg_si/ $(RXMLDIR)
+       $(H)scp $^ $(RDOWNDIR)
+       $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf download/lddl.tar.bz2"
+
+#      $(H)scp -r $(XMLDIR) $(RXMLDIR)
 
 test-html:
        @$(MAKE) --no-print-directory $(XMLS:%.xml=%)
@@ -126,7 +131,7 @@ install-contrib: $(CONTRIB:%=$(CONTRIBDIR)/%)
        $(H)scp $< $(DOWNDIR)
 
 up:
-       @echo "  UPDATE $(REMOTE):$(RDIR)"
+       @echo "  UPDATE $(RHOMEDIR)"
        $(H)ssh $(REMOTE) "svn up $(RDIR)"
 
 %.ld:

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 31b4d9c92322a4593cec95fbf96c90395883265d..5184a4d124aea90b5d754c53e9cf4afb2429fa88 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -142,29 +142,29 @@
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">4</td>
+            <td class="snnn right italic cyan">14</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">68581</td>
+            <td class="snnn right italic cyan">6787</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">3637</td>
+            <td class="ssnn right italic cyan">10070</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
             <td class="snnn right italic green">2</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1</td>
+            <td class="snnn right italic green">4</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">3</td>
+            <td class="ssnn right italic green">6</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">3</td>
+            <td class="snsn right italic yellow">6</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">9</td>
+            <td class="snsn right italic yellow">11</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">12</td>
+            <td class="sssn right italic yellow">17</td>
           </tr>
         </tbody>
       </table>
@@ -250,6 +250,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:52 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index e67e7d200a6807b1c5fb552290938d59bd3474c6..353b1c74e3a13c93f716eb4661aef787e5b5fb37 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -126,7 +126,7 @@
             <td class="snns italic cyan">characters</td>
             <td class="snnn right italic cyan">433402</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1874774</td>
+            <td class="ssnn right italic cyan">1874778</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
@@ -1366,6 +1366,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:52 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 38d99b003b434f22c4818005996ef44292537fba..8d7d6b75364fcf1502d248495eb105a3ea1a4936 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -358,6 +358,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/download/lddl.tar.bz2 b/helm/www/lambdadelta/download/lddl.tar.bz2
index 06b341d98efb6511bc210233967a34708e949c24..0237443ce5ebacac799d4b1897d7973a3c611770 100644 (file)
Binary files a/helm/www/lambdadelta/download/lddl.tar.bz2 and b/helm/www/lambdadelta/download/lddl.tar.bz2 differ

diff --git a/helm/www/lambdadelta/etc/exclude.txt b/helm/www/lambdadelta/etc/exclude.txt
new file mode 100644 (file)
index 0000000..c9a35c9
--- /dev/null
+++ b/helm/www/lambdadelta/etc/exclude.txt
@@ -0,0 +1 @@
+xml/.svn

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index e5218996f8e362497548f1df7f8acb5b337263e0..7f5ada5fd4507a58f1d1793ed569cd74cba67166 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -123,7 +123,7 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">30</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">68581</td>
+            <td class="snnn right italic cyan">46649</td>
             <td class="snns italic cyan">nodes</td>
             <td class="ssnn right italic cyan">62380</td>
           </tr>
@@ -288,6 +288,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:52 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 9b819674c93578d2f0faf7e39b8c0118e48312d6..2881bbd7607aece6816f2548074f8b28ca0d094a 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -111,8 +111,8 @@
       <li>
       <span class="emph alpha">Access:</span>
       <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="emph beta">2012-10</span>),
-      <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph beta">2012-10</span>),
-      <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph beta">2012-10</span>).
+      <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="emph beta">2014-12</span>),
+      <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="emph beta">2014-12</span>).
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/" id="examples">
@@ -145,12 +145,19 @@
       <li>
       <span class="emph beta">Version 0.8.2.</span>
       In progress.
+      <ul>
+          <li>
+         <span class="emph gamma">2014-12.</span>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in λδ "Version 3".
+      </li>
+        </ul>
    </li>
     </ul>
    <ul xmlns:ld="http://lambdadelta.info/" id="v1">
       <li>
       <span class="emph beta">Version 0.8.1 (2010-11).</span>
-      Exploits a subset of "complete_rg" λδ as the intermediate language.
+      Uses a subset of λδ "Version 4" as the intermediate language.
       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"
       increases of 22% with respect to version 0.8.0.
@@ -174,7 +181,7 @@
    <ul xmlns:ld="http://lambdadelta.info/" id="v0">
       <li>
       <span class="emph beta">Version 0.8.0 (2009-09).</span>
-      Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+      Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
       <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
@@ -226,6 +233,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 23:26:17 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index d1c9cff59088906b0233b4be120c3da5279fb57e..07297ff24e9e18709491959e437890cbdbd0d905 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -200,6 +200,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 888e497ca92836a9ccd40d6ef91caa7003298d01..110c880fb2f87743227aeccfaa8a6f824638ac40 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -325,6 +325,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:51 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 0c02414008a49a22f41ac8eccfc4177610ff1a00..857add671f9a38a0f2329f1454e1ad5258725689 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -309,6 +309,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 04 Nov 2014 16:28:51 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 24 Dec 2014 22:58:52 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index 48ff2c594966c98553b5b4c4493630fa35bd25ca..8e27e166b780f17a4fa1ee1e755f05b190012a05 100644 (file)
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -22,8 +22,8 @@
    <topitem name="access">
       <notice class="alpha" notice="Access:"/>
       <rlink to="static/lddl/">static pages</rlink> (updated <notice class="beta" notice="2012-10"/>),
-      <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="beta" notice="2012-10"/>),
-      <rlink to="xml/">HELM server URL</rlink> (updated <notice class="beta" notice="2012-10"/>).
+      <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="beta" notice="2014-12"/>),
+      <rlink to="xml/">HELM server URL</rlink> (updated <notice class="beta" notice="2014-12"/>).
    </topitem>
    <topitem name="examples">
       <notice class="alpha" notice="Examples:"/>
@@ -51,10 +51,15 @@
    <topitem name="v2">
       <notice class="beta" notice="Version 0.8.2."/>
       In progress.
+      <list><item>
+         <notice class="gamma" notice="2014-12."/>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in λδ "Version 3".
+      </item></list>
    </topitem>
    <topitem name="v1">
       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
-      Exploits a subset of "complete_rg" λδ as the intermediate language.
+      Uses a subset of λδ "Version 4" as the intermediate language.
       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"
       increases of 22% with respect to version 0.8.0.
@@ -73,7 +78,7 @@
    </topitem>
    <topitem name="v0">
       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
-      Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+      Supports λδ "Version 2" with naive implementation of impredicative sort inclusion.
       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
       <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.

diff --git a/helm/www/lambdadelta/xml/ld.dtd b/helm/www/lambdadelta/xml/ld.dtd
index a01238d91fb694483d9f9add7a73cbffb7c8b395..0fb547e45bf00fbc2557662ca92ebb488f9c65a2 100644 (file)
--- a/helm/www/lambdadelta/xml/ld.dtd
+++ b/helm/www/lambdadelta/xml/ld.dtd
@@ -45,7 +45,7 @@
 
 <!ELEMENT Abst %term;>
 <!ATTLIST Abst
-          level    NMTOKEN #IMPLIED
+          layer    NMTOKEN #IMPLIED
           position NMTOKEN #REQUIRED
          name     NMTOKEN #IMPLIED
 >
@@ -88,4 +88,5 @@
 <!ATTLIST CONSTANT
           xmlns     CDATA    #FIXED    "http://lambdadelta.info/"
          hierarchy NMTOKEN  #REQUIRED
+          options   NMTOKENS #IMPLIED
 >