From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Thu, 21 Nov 2019 23:12:52 +0000 (+0100)
Subject: web site update
X-Git-Tag: make_still_working~216
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ec8ae0a49716b205bbf63568ee625ec1e9eb524;p=helm.git
web site update
+ some links fixed
+ minor corrections
---
diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile
index e9008a950..76705a3f8 100644
--- 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 e2b6c590c..e8d861ee1 100644
--- 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 64ffcf1af..2fedd9675 100644
--- 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 3538b68d9..de56d6a08 100644
--- 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 ecd3ffabf..3a2740198 100644
--- 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 fa16e0667..187dd1b99 100644
--- 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") * }