From 644307df315b855c3851f813b04d562acf2db9bc Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 20 Jul 2014 13:17:56 +0000 Subject: [PATCH] the generation of the web site is completed! --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 2 +- helm/www/lambdadelta/basic_2.html | 2 +- helm/www/lambdadelta/documentation.html | 12 +- helm/www/lambdadelta/ground_2.html | 2 +- helm/www/lambdadelta/implementation.html | 513 +++++++++--------- helm/www/lambdadelta/index.html | 53 +- helm/www/lambdadelta/news.html | 8 +- helm/www/lambdadelta/version_1.html | 8 +- helm/www/lambdadelta/version_2.html | 8 +- .../web/home/implementation.ldw.xml | 99 ++++ helm/www/lambdadelta/web/home/index.ldw.xml | 5 - helm/www/lambdadelta/web/home/sitemap.tbl | 9 +- helm/www/lambdadelta/xslt/ld_web_root.xsl | 20 +- 14 files changed, 417 insertions(+), 326 deletions(-) create mode 100644 helm/www/lambdadelta/web/home/implementation.ldw.xml diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 9b46aa52c..a477e6d4f 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index ece3b07ca..fb588eea5 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 9595ea5b3..3bcd218b0 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1300,6 +1300,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index e41618049..e1e583101 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -42,9 +42,9 @@ implementation - -
- + (specifications + library + Helena) @@ -96,7 +96,7 @@
- [basic lambdadelta] λδ version 2 (in progress)
+ [basic lambdadelta logo] λδ version 2 (in progress)
The main source of information is P8.
@@ -180,7 +180,7 @@
- [basic lambdadelta] λδ version 1 (dismissed)
+ [basic lambdadelta logo] λδ version 1 (dismissed)
The main source of information is J1. A summary is available in P5. @@ -327,6 +327,6 @@

-
Last update: Sun, 20 Jul 2014 11:35:27 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 32705c284..810064210 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -234,6 +234,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index cb9b23247..77a7b0f29 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -1,255 +1,274 @@ - - - + + + + + + + + + + \lambda\delta home page + + + + + + +
+ + [lambdadelta home] + +
+
The Formal System λδ (\lambda\delta)
+
+ [Spacer] +
+
+
+
+
+ + + + + + + + + + + + + + + + + + + + + + + + +
+ home + + news + + documentation + + implementation + (specifications + library + Helena)
+ Foreword + + Milestones + + Version 2 + + Version 2 + + Background + Core + Applications +
+ Notice + + Visibility + + Version 1 + + Version 1 + +
+
+
- - λδ home page - - - - -
-
- [Crux Logo] -

The Formal System λδ (\lambda\delta)
-

-

Towards the unification of terms, types, environments and - contexts

- [Separator]
- +
Computer-checked formal specifications [spacer] +
+
+ λδ comes in several versions listed in the following table, + which includes the major milestones: +
+
+
- - + + + + + + + + + + + + + + + + + + + + + + + +
- - - -
    -
  • Resources
    -
    • -
- 		-

Computer-checked formal - specifications [Butterfly]

- Resource - 1 below provides for the statically generated natural language - representation of - λδ meta-theory (faster rendering w.r.t. resource 2 below).
- Resource 2 below - provides - for the dynamically generated natural - language representation of - λδ meta-theory (powered by the HELM - rendering engine).
- Remarkably, λδ was born and developed in the digital - format of resource 3 - below, which is not the - formal counterpart of some informal material previously - written on - paper (as it happens for most currently digitalized - Mathematics).
-
    -
  1. F. Guidi: lambdadelta - (revised 2011-09). - Formal - specification for Matita 0.5 - (HTML pages generated - by the HELM - rendering engine) - Here are the most relevant theorems proved in the - formal specification: - -
    2. -
  2. F. Guidi: lambdadelta - (revised 2011-09). - Formal - specification for Matita 0.5 (HELM directory).
    - Currently, the HELM rendering engine is offline.
    -
    -
    3. -
  3. F. Guidi: lambdadelta_1 - (revised 2012-10). -Formal - specification for Coq - 7.3.1 - (source - proof scripts). BibTeX entry.
    -
    4. -
-

Tools [Butterfly]

- [Crux Logo] The λδ - Digital - Library - (LDDL) is part of HELM - and contains a set of - resources expressed in λδ.
-
    -
  • Contents: - Landau's "Grundlagen - der Analysis" (from - Jutting's specification in Automath).
    -
    • -
- - -
- [Helena Logo] Helena - is a λδ - processor, - implemented in Caml - as a part of - the HELM software, - meant for - testing the stable features of the calculus as well as the - unstable - ones.
- The processor source code is available in the directory /trunk/helm/software/helena/ - of the HELM - Svn - repository. The Svn revisions containing the stable - versions - of  Helena are indicated below.
-
    -
  • Version 0.8.2. - In - progress.
    -
    • -
-
    -
  • Version 0.8.1 - (2010-11). - Exploits a subset of "complete_rg" λδ 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. [Svn - revision: 11032] (archived - source code) - -
    • -
-
    -
  • Version 0.8.0 (2009-09). - Supports - "basic_rg" λδ with naive implementation of - impredicative sort - inclusion. Features - importation from Automath - and exportation to XML. - [Svn - revision: 10304] (archived - source code)
    -
      -
    • 2009-09. - Jutting's specification of Landau's "Grundlagen - der - Analysis" enters λδ Digital Library.
      -
      • -
    • 2009-06. - Jutting's specification of Landau's "Grundlagen - der - Analysis" is - successfully processed, enabling sort inclusion.
      • -
    -
    • -
-

Other resources [Butterfly]

- -
    -
  • A Jed mode - for - editing ".hln" files (containing λδ textual syntax): helena.sl - (revised 2010-11).
    • -
- -
    -
  • A logo for λδ: crux_177.png - (revised 2012-09).
    -
    • -
+ 		versionnamedeveloped withstartedannouncedreleaseddismissed
2 + basic_2 + + Matita 0.99.2 + April 2011July 2014Planned in 2014Not planned yet
1 + basic_1 + + Coq 7.3.1 May 2004January 2006November 2006May 2008
-
- [Valid HTML 4.01 Transitional] [Use Any - Browser Here] [PNG Used Here]
-
- Last update 2014-02-22 by Ferruccio - Guidi
- - + +
Tools [spacer] +
+ +
+ [Crux logo] λδ Digital Library (LDDL)
+
+ The λδ Digital Library is part of HELM + and contains resources expressed in λδ. +
+ + + + +
+ [Helena logo] Helena
+
+ Helena is a λδ processor, + implemented in Caml + as a part of the HELM software, + meant for testing the stable features of the calculus as well as the unstable ones. +
+
+ The processor source code is available in the directory + /trunk/helm/software/helena/ + of the HELM Svn repository. + The Svn revisions containing the stable versions of Helena are indicated next. +
+ + + +
+ [Spacer] +
+
+
+
+
+ + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
+
+
+
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
+ + diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index e6e6a2434..3f33aa057 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -42,9 +42,9 @@ implementation - -
- + (specifications + library + Helena) @@ -100,51 +100,6 @@ as a machine-checked digital specification that is not the formal counterpart of some previously published informal material.
-
- λδ comes in several versions listed in the following table, - which includes the major milestones: -
-
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
versionnamedeveloped withstartedannouncedreleaseddismissed
2 - basic_2 - - Matita 0.99.2 - April 2011July 2014Planned in 2014Not planned yet
1 - basic_1 - - Coq 7.3.1 - May 2004January 2006November 2006May 2008
-
This is the System logo: crux_177.png (revised 2012-09). @@ -186,6 +141,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index f526a75a9..54a3d4af6 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -42,9 +42,9 @@ implementation - -
- + (specifications + library + Helena) @@ -286,6 +286,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index 856c396a8..1549b10d6 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -42,9 +42,9 @@ implementation - -
- + (specifications + library + Helena) @@ -169,6 +169,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index 530f2ad47..bbbf58ff7 100644 --- a/helm/www/lambdadelta/version_2.html +++ b/helm/www/lambdadelta/version_2.html @@ -42,9 +42,9 @@ implementation - -
- + (specifications + library + Helena) @@ -134,6 +134,6 @@

-
Last update: Sun, 20 Jul 2014 11:29:55 +0200
+
Last update: Sun, 20 Jul 2014 15:02:32 +0200
diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml new file mode 100644 index 000000000..b8cc30553 --- /dev/null +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -0,0 +1,99 @@ + + + + + + Computer-checked formal specifications + + λδ comes in several versions listed in the following table, + which includes the major milestones: + + + + Tools + +
λδ Digital Library (LDDL)
+ + The λδ Digital Library is part of HELM + and contains resources expressed in λδ. + + + Landau's "Grundlagen der Analysis" + (from Jutting's specification in Automath). + + + static pages (updated ), + data set (updated ), + HELM server URL (updated ). + + + + Grundlagen's definition "t234" + (in "basic_rg" λδ), + + Grundlagen's definition "t234" + (in "complete_rg" λδ). + + +
Helena
+ + Helena is a λδ processor, + implemented in Caml + as a part of the HELM software, + meant for testing the stable features of the calculus as well as the unstable ones. + + + The processor source code is available in the directory + /trunk/helm/software/helena/ + of the HELM Svn repository. + The Svn revisions containing the stable versions of Helena are indicated next. + + + In progress. + + + Exploits a subset of "complete_rg" λδ 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 toversion 0.8.0. + [Svn revision: 11032] (archived source code) + + A Jed mode + for editing ".hln" files (containing λδ textual syntax): + helena.sl + (revised ). + + + Helena appears in F. Wiedijk's + + index of computer math systems. + + + + Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion. + Features importation from Automath + and exportation to XML. + Documentation. + [Svn revision: 10304] (archived source code). + + A Jed mode + for editing ".aut" files + (containing Automath textual syntax): + automath.sl + (revised ). + + + Jutting's specification of Landau's "Grundlagen der Analysis" + enters λδ Digital Library. + + + Jutting's specification of Landau's "Grundlagen der Analysis" + is successfully processed, enabling sort inclusion. + + +
+ diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml index 1b6c27c19..677e33bd9 100644 --- a/helm/www/lambdadelta/web/home/index.ldw.xml +++ b/helm/www/lambdadelta/web/home/index.ldw.xml @@ -20,11 +20,6 @@ as a machine-checked digital specification that is not the formal counterpart of some previously published informal material. - - λδ comes in several versions listed in the following table, - which includes the major milestones: - -
This is the System logo: crux_177.png (revised ). diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index 71cc44367..9ee265a89 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -17,9 +17,14 @@ table [ [ @@("documentation#v1" "Version 1") * ] } class "green" { - [ @@"implementation" * ] + [ @@"implementation" + "(" ^ @@("implementation#specifications" "specifications") + + @@("implementation#lddl" "library") + + @@("implementation#helena" "Helena") ^ ")" + * ] [ @@("version_2" "Version 2") - @@("ground_2" "Background") + @@("basic_2" "Core") + @@("apps_2" "Applications") * ] + @@("ground_2" "Background") + @@("basic_2" "Core") + @@("apps_2" "Applications") + * ] [ @@("version_1" "Version 1") * ] * } ] diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index 2eef8f149..d0024b8dc 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -120,13 +120,31 @@ [basic lambdadelta] + + [Crux logo] + + + + + [Helena logo] + + +

-- 2.39.2