From 2ec8ae0a49716b205bbf63568ee625ec1e9eb524 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 22 Nov 2019 00:12:52 +0100 Subject: [PATCH] web site update + some links fixed + minor corrections --- helm/www/lambdadelta/Makefile | 2 +- helm/www/lambdadelta/web/home/documentation_1.tbl | 2 +- helm/www/lambdadelta/web/home/documentation_2.tbl | 4 ++-- helm/www/lambdadelta/web/home/news.ldw.xml | 2 +- helm/www/lambdadelta/web/home/specification.ldw.xml | 4 ++-- helm/www/lambdadelta/web/home/versions.tbl | 11 +++++++---- 6 files changed, 14 insertions(+), 11 deletions(-) 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" "V1a." "" } { "F. Guidi:" + - @@("html/version_1.html" "lambdadelta_1A") + + @@("html/specification.html#source1A" "lambdadelta_1A") + "(revised 2019-11)." + "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" "V2b." "" } { "F. Guidi:" + - @@("html/version_2.html" "lambdadelta_2B") + + @@("html/specification.html#source2B" "lambdadelta_2B") + "(revised 2019-11)." + "Formal specification for the proof assistant Matita 0.99.4 (scripts)." + @@("html/documentation.html#bibtex" "BibTeX entry") ^ "." @@ -94,7 +94,7 @@ table { ] [ { name "ldV2a" "V2a." "" } { "F. Guidi:" + - @@("html/version_2.html" "lambdadelta_2A") + + @@("html/specification.html#source2A" "lambdadelta_2A") + "(revised 2019-11)." + "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. - + The corrected specification of Landau's "Grundlagen der Analysis" is validated in a Î»Prolog implementation of Î»Î´-3. 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 @@ the scripts are checked by the latest version of Matita from - helm.git repository. + HELM Git repository. lambdadelta_2B for Matita 0.99.4 - (revised ). + (revised ). Source scripts [Git revision: 2019-11-19 20:45:15]. Documentation (V2b). 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") * } -- 2.39.2