]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: dd731f0)
web site update
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Thu, 21 Nov 2019 23:12:52 +0000 (00:12 +0100)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Thu, 21 Nov 2019 23:12:52 +0000 (00:12 +0100)
+ some links fixed
+ minor corrections

helm/www/lambdadelta/Makefile patch | blob | history
helm/www/lambdadelta/web/home/documentation_1.tbl patch | blob | history
helm/www/lambdadelta/web/home/documentation_2.tbl patch | blob | history
helm/www/lambdadelta/web/home/news.ldw.xml patch | blob | history
helm/www/lambdadelta/web/home/specification.ldw.xml patch | blob | history
helm/www/lambdadelta/web/home/versions.tbl patch | blob | history

diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index e9008a950c30a13b68e2dba934c0aa5991b00610..76705a3f88c2fe0330d3f97a9e3cf3164f219343 100644 (file)
--- a/helm/www/lambdadelta/Makefile
+++ b/helm/www/lambdadelta/Makefile
@@ -155,7 +155,7 @@ install-1: etc/coq/ld_731/contrib/lambdadelta.tar.gz
 
 install-coq:
        @echo "  INSTALL coq"
-       $(H)ssh $(REMOTE) "cd $(RSTATICDIR)/coq && tar -xzf ../../../lambdadelta/download/lambdadelta_1.tar.gz && . ../../../lambdadelta/etc/to_text.sh v"
+       $(H)ssh $(REMOTE) "cd $(RSTATICDIR)/coq && tar -xjf ../../../lambdadelta/download/lambdadelta_1A.tar.bz2 && . ../../../lambdadelta/etc/to_text.sh v"
 
 install-v: $(HELENADIR)/$(COQ)
        @echo "  INSTALL $(notdir $<)"
diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl
index e2b6c590cd22001e00470efd8f8d119fdf56ccb1..e8d861ee15325e0046b9e04006dfaef015055315 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_1.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_1.tbl
@@ -88,7 +88,7 @@ table {
    ]
    [ { name "ldV1a" "<span class=\"emph alpha\">V1a.</span>" "" } {
      "F. Guidi:" +
-     @@("html/version_1.html" "lambdadelta_1A") +
+     @@("html/specification.html#source1A" "lambdadelta_1A") +
      "(revised <span class=\"emph delta\">2019-11</span>)." +
      "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 64ffcf1af8885adaa792c0d6a79542f247028c8e..2fedd967572ba93fded847f255cc322fb07c3026 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation_2.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_2.tbl
@@ -86,7 +86,7 @@ table {
    ]
    [ { name "ldV2b" "<span class=\"emph alpha\">V2b.</span>" "" } {
      "F. Guidi:" +
-     @@("html/version_2.html" "lambdadelta_2B") +
+     @@("html/specification.html#source2B" "lambdadelta_2B") +
      "(revised <span class=\"emph gamma\">2019-11</span>)." +
      "Formal specification for the proof assistant Matita 0.99.4 (scripts)." +
      @@("html/documentation.html#bibtex" "BibTeX entry") ^ "."
@@ -94,7 +94,7 @@ table {
    ]
    [ { name "ldV2a" "<span class=\"emph alpha\">V2a.</span>" "" } {
      "F. Guidi:" +
-     @@("html/version_2.html" "lambdadelta_2A") +
+     @@("html/specification.html#source2A" "lambdadelta_2A") +
      "(revised <span class=\"emph delta\">2019-11</span>)." +
      "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 3538b68d91778edff2dd01cf7342ffd6eda8e72a..de56d6a08b1aa543efac0ffcd213e7d0ee586c1c 100644 (file)
--- a/helm/www/lambdadelta/web/home/news.ldw.xml
+++ b/helm/www/lambdadelta/web/home/news.ldw.xml
@@ -46,7 +46,7 @@
       The specification of λδ-2A is concluded.
    </news>
 
-   <news class="gamma" date="June 2015.">
+   <news class="alpha" date="June 2015.">
       The corrected specification of Landau's "Grundlagen der Analysis"
       is validated in a λProlog implementation of λδ-3.
    </news>
diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index ecd3ffabf4292b9cdc158d45516776a65d21f1a7..3a2740198f2af90ab8fab741cb0036d1bc3f0272 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -77,13 +77,13 @@
    <body>
       <notice class="alpha" text="Notice:"/>
       the scripts are checked by the latest version of Matita from
-      <link to="http://matita.cs.unibo.it/gitweb/">helm.git repository</link>.
+      <link to="http://matita.cs.unibo.it/gitweb/?p=helm.git;a=summary">HELM Git repository</link>.
    </body>
 
    <topitem name="source2B">
       <body>
          <rlink to="download/lambdadelta_2B.tar.bz2">lambdadelta_2B for Matita 0.99.4</rlink>
-         (revised <notice class="delta" text="2019-11"/>).
+         (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>.
       </body>
diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl
index fa16e06671b3ce3c29111ef0cb9a0608af14f811..187dd1b990946ae48cd8d948535b79a57460677a 100644 (file)
--- a/helm/www/lambdadelta/web/home/versions.tbl
+++ b/helm/www/lambdadelta/web/home/versions.tbl
@@ -8,10 +8,13 @@ table {
         "references"
       ]
    class "yellow"
-      [ @@("html/specification#v3" "Version 3") "\"basic_3\""
-        "" ""
-        "" "" "" ""
-        @@("html/documentation#ldJ3a" "J3a")
+      [ { @@("html/specification#v3" "Version 3") *}
+        { "\"basic_3\"" * }
+        { [ "" ""
+            "" "" "" ""
+            @@("html/documentation#ldJ3a" "J3a")
+          ]
+        }
       ]
    class "orange" {
       [ { @@("html/specification#v2" "Version 2") * }
Unnamed repository; edit this file 'description' to name the repository.