From: Ferruccio Guidi Date: Sun, 29 Jun 2014 20:28:24 +0000 (+0000) Subject: - we begin the new site based on ld_web X-Git-Tag: make_still_working~888 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=cb0d4e730bd6ec9bed1018be37748120f740f0a9 - we begin the new site based on ld_web - xhtbl: xml namespaces and absolute atnl links are now supported - lambdadelta_2 uploaded --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index b23abc990..2e1bdeeb4 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -23,7 +23,8 @@

-

Character classes

Character classes

This table shows how the first 45 positive integers are distributed in the four classes.

@@ -223,6 +224,6 @@

Last update: Sat, 28 Jun 2014 20:29:31 +0200

Last update: Sun, 29 Jun 2014 22:20:18 +0200

diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 3a34b41d8..3533cb02e 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -3,20 +3,21 @@ H=@ TAGS = www up \ lint-xml index lddl install-xml \ test-html html install-html \ - install-jed install-bib \ + install-jed install-bib install-contrib \ LDURL = http://lambdadelta.info/ HOMEDIR = . -ETCDIR = etc -DOWNDIR = download -XSLTDIR = xslt -XMLDIR = xml -SRCDIR = web/home -XHTBLDIR = bin/xhtbl -HTMLDIR = $(HOME)/public_html/lddl -JEDDIR = $(HOME)/mps/jed -BIBDIR = $(HOME)/texmf/bibtex/bib +ETCDIR = etc +DOWNDIR = download +XSLTDIR = xslt +XMLDIR = xml +SRCDIR = web/home +XHTBLDIR = bin/xhtbl +HTMLDIR = $(HOME)/public_html/lddl +JEDDIR = $(HOME)/mps/jed +BIBDIR = $(HOME)/texmf/bibtex/bib +CONTRIBDIR = $(ETCDIR)/lambdadelta WEBDIRS = $(SRCDIR) $(ETCDIR) @@ -25,8 +26,9 @@ RDIR = /projects/helm/public_html/lambdadelta RXMLDIR = $(REMOTE):$(RDIR)/xml RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl -SLS = helena.sl automath.sl -BIB = lambdadelta.bib +SLS = helena.sl automath.sl +BIB = lambdadelta.bib +CONTRIB = lambdadelta_2.tar.gz XMLS = brg_si/grundlagen/l/not.ld.xml \ brg_si/grundlagen/l/et.ld.xml \ @@ -124,6 +126,11 @@ install-bib: $(BIB:%=$(BIBDIR)/%) @echo " INSTALL $(BIB)" $(H)scp $< $(DOWNDIR) $(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt) + +install-contrib: $(CONTRIB:%=$(CONTRIBDIR)/%) + @echo " INSTALL $(CONTRIB)" + $(H)scp $< $(DOWNDIR) + up: @echo " UPDATE $(REMOTE):$(RDIR)" $(H)ssh $(REMOTE) "svn up $(RDIR)" diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 3bd4980e4..3aaefb691 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -23,7 +23,8 @@

Contents of the Specification

Contents of the Specification

This specification comprises a collection of checked applications of Î»Î´ version 2. In particular it contains the components below. @@ -43,7 +44,8 @@ -

Summary of the Specification

Summary of the Specification

Here is a numerical acount of the specification's contents and its timeline. Nodes are counted according to the "intrinsinc complexity measure" @@ -55,21 +57,21 @@ - - - + + - - - - @@ -123,7 +125,8 @@ -

Logical Structure of the Specification

Logical Structure of the Specification

The source files are grouped in planes and components according to the following table. Each component contains its own notation file. @@ -134,10 +137,10 @@

- - - - + + + @@ -161,7 +164,8 @@

Physical Structure of the Specification

Physical Structure of the Specification

The source files are grouped in directories, one for each component.

@@ -191,6 +195,6 @@

Last update: Sat, 28 Jun 2014 20:29:31 +0200

Last update: Sun, 29 Jun 2014 22:20:18 +0200

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 8e5745e16..5e4cb7ef6 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -25,7 +25,8 @@

Summary of the Specification

Summary of the Specification

Here is a numerical acount of the specification's contents and its timeline. Nodes are counted according to the "intrinsinc complexity measure" @@ -37,21 +38,21 @@ - - - + + - - - - @@ -208,7 +209,8 @@ -

Logical Structure of the Specification

Logical Structure of the Specification

The source files are grouped in planes and components according to the following table. Notation files covering the whole specification are provided. @@ -219,16 +221,16 @@

- - - - + + + - - @@ -1242,7 +1244,8 @@

Physical Structure of the Specification

Physical Structure of the Specification

The source files are grouped in directories, one for each component.

@@ -1272,6 +1275,6 @@

Last update: Sat, 28 Jun 2014 20:29:31 +0200

Last update: Sun, 29 Jun 2014 22:20:18 +0200

diff --git a/helm/www/lambdadelta/bin/xhtbl/matrix.ml b/helm/www/lambdadelta/bin/xhtbl/matrix.ml index 4769a5457..86d6f053a 100644 --- a/helm/www/lambdadelta/bin/xhtbl/matrix.ml +++ b/helm/www/lambdadelta/bin/xhtbl/matrix.ml @@ -3,7 +3,7 @@ module A = Array module T = Table type cell = { - ck: string list; (* contents *) + ck: T.text list; (* contents *) cc: T.css; (* css classes *) cb: T.border; (* border *) } diff --git a/helm/www/lambdadelta/bin/xhtbl/table.ml b/helm/www/lambdadelta/bin/xhtbl/table.ml index e363cd434..204df4c90 100644 --- a/helm/www/lambdadelta/bin/xhtbl/table.ml +++ b/helm/www/lambdadelta/bin/xhtbl/table.ml @@ -17,7 +17,10 @@ type border = { w: bool; (* west *) } -type key = Text of string list +type text = Plain of string + | Link of string * string + +type key = Text of text list | Glue of int option type table = { diff --git a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll index 0f61349c3..7efa9035d 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textLexer.mll +++ b/helm/www/lambdadelta/bin/xhtbl/textLexer.mll @@ -16,16 +16,20 @@ rule token = parse | QT { let s = str lexbuf in out s; TP.TEXT s } | NUM as s { out s; TP.NUM (int_of_string s) } + | "(*" { block lexbuf; token lexbuf } | "{" { out "{"; TP.OC } | "}" { out "}"; TP.CC } | "[" { out "["; TP.OB } | "]" { out "]"; TP.CB } | "*" { out "*"; TP.SR } | "+" { out "+"; TP.PS } + | "(" { out "("; TP.OP } + | ")" { out ")"; TP.CP } + | "@" { out ")"; TP.AT } + | "space" { out "name"; TP.SPACE } | "name" { out "name"; TP.NAME } | "table" { out "table"; TP.TABLE } | "class" { out "class"; TP.CSS } - | "(*" { block lexbuf; token lexbuf } | eof { TP.EOF } and str = parse | QT { "" } diff --git a/helm/www/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly index 333d3421f..3864bc53c 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textParser.mly +++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly @@ -15,15 +15,26 @@ let mk_atom s rs = %token NUM %token TEXT -%token NAME TABLE CSS SR OC CC OB CB PS EOF +%token SPACE NAME TABLE CSS SR OC CC OB CB PS OP CP AT EOF %start script -%type <(string * Table.table * Css.atoms) list> script +%type <(string * string) list * (string * Table.table * Css.atoms) list> script %% +space: + | SPACE TEXT TEXT { $2, $3 } +; + +spaces: + | { [] } + | space spaces { $1 :: $2 } +; + text: - | TEXT { $1 } + | TEXT { T.Plain $1 } + | AT OP TEXT TEXT CP { T.Link ($3, $4) } +; texts: | text { [$1] } @@ -89,7 +100,11 @@ directive: | name TABLE table atoms { $1, $3, $4 } ; +directives: + | { [] } + | directive directives { $1 :: $2 } +; + script: - | EOF { [] } - | directive script { $1 :: $2 } + | spaces directives EOF { $1, $2 } ; diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml index 54995e96b..fec699bcb 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml @@ -41,10 +41,12 @@ let border tb = let css tc = P.sprintf "\"%s\"" (S.concat " " tc) +let text = function + | T.Plain s -> P.sprintf "\"%s\"" s + | T.Link (uri, s) -> P.sprintf "@(\"%s\" \"%s\")" uri s + let key = function - | T.Text sl -> - let map s = P.sprintf "\"%s\"" s in - S.concat " + " (L.map map sl) + | T.Text sl -> S.concat " + " (L.map text sl) | T.Glue None -> "*" | T.Glue (Some i) -> P.sprintf "%u" i diff --git a/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml index dc4ab9670..f379185fa 100644 --- a/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml +++ b/helm/www/lambdadelta/bin/xhtbl/xhtbl.ml @@ -51,9 +51,10 @@ let process_file fname = let bname = F.chop_extension (F.basename fname) in let ich = open_in fname in let lexbuf = Lexing.from_channel ich in - let ds = TP.script TL.token lexbuf in + let ns, ds = TP.script TL.token lexbuf in close_in ich; includes := bname :: !includes; - let och = XU.open_out true bname in + let ns = ("", "http://www.w3.org/1999/xhtml") :: ns in + let och = XU.open_out bname ns in L.iter (process_directive och bname) ds; XU.close_out och diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml index 3583c2f75..f413aa0ef 100644 --- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml @@ -22,8 +22,12 @@ let border cell = if cell.M.cb.T.w then str.[3] <- 's'; str :: cell.M.cc +let text = function + | T.Plain s -> s + | T.Link (uri, s) -> P.sprintf "%s" uri s + let key cell = - if cell.M.ck = [] then "
" else S.concat " " cell.M.ck + if cell.M.ck = [] then "
" else S.concat " " (L.map text cell.M.ck) let ind i = S.make (2 * i) ' ' @@ -37,16 +41,20 @@ let out_row och row = A.iter (out_cell och) row; P.fprintf och "%s\n" (ind (i+3)) +let out_space och (name, uri) = + let name = if name = "" then name else ":" ^ name in + P.fprintf och " xmlns%s=\"%s\"\n" name uri + (****************************************************************************) -let open_out html name = +let open_out name spaces = let fname = F.concat !O.output_dir (P.sprintf "%s.xsl" name) in + let spaces = ("xsl", "http://www.w3.org/1999/XSL/Transform") :: spaces in let och = open_out fname in P.fprintf och "\n\n"; P.fprintf och "\n\n" msg; P.fprintf och "\n\n"; och @@ -72,7 +80,7 @@ let map_tbls och name = P.fprintf och "%s\n" (ind (i+2)) let write_hook name incs tbls = - let och = open_out false name in + let och = open_out name [] in L.iter (map_incs och) incs; P.fprintf och "\n\n" name; P.fprintf och "%s\n" (ind (i+1)); diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index 9e7c3fc08..ed3a266f5 100644 --- a/helm/www/lambdadelta/css/ld_web.css +++ b/helm/www/lambdadelta/css/ld_web.css @@ -10,16 +10,20 @@ body { a:link, a:visited { text-decoration: underline; + color: rgb(0, 0, 0); } a:active, a:hover, a:focus { background: rgb(192, 192, 192); + color: rgb(0, 0, 0); } /* blocks *******************************************************************/ div.spacer { text-align: center; + font-weight: normal; + font-size: medium; } div.head1 { @@ -29,20 +33,30 @@ div.head1 { font-size: xx-large; } -div.head2 { +div.head2sn { margin: 0.5em 0; text-align: left; font-weight: bold; font-size: x-large; } +div.head2dx { + margin: 0.5em 0; + text-align: right; + font-weight: bold; + font-size: x-large; +} + div.text { margin: 1em 0; text-align: left; + font-weight: normal; + font-size: medium; } span.date { font-weight: bold; + font-size: medium; } /* inline decorations *******************************************************/ @@ -53,6 +67,12 @@ img.icon32 { height: 32px; } +img.icon37 { + border: 0; + width: 37px; + height: 37px; +} + img.rule { border: 0; height: 4px; @@ -68,7 +88,7 @@ img.w3c { /* background colors ********************************************************/ -.grey { +.gray { background-color:#dfdfdf; /* + 7/8 */ } diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index 5b5eb1d97..580d39fcf 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -1,3 +1,14 @@ +% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +@misc{lambdadelta8, + author="F. {Guidi}", + title="{lambdadelta\_2}", + howpublished="Formal specification for the proof assistant Matita 0.99.2", + year="2014", + month="July", + note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" +} + @incollection{lambdadelta7, author="F. {Guidi}", title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", @@ -21,6 +32,8 @@ month="September" } +% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + @article{lambdadelta5, author="F. {Guidi}", title="{The Formal System $\lambda\delta$}", @@ -71,7 +84,7 @@ @misc{lambdadelta1, author="F. {Guidi}", title="{lambdadelta\_1}", - howpublished="Formal specification with the proof assistant Coq 7.3.1", + howpublished="Formal specification for the proof assistant Coq 7.3.1", year="2006", month="November", note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index 5b5eb1d97..580d39fcf 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -1,3 +1,14 @@ +% \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +@misc{lambdadelta8, + author="F. {Guidi}", + title="{lambdadelta\_2}", + howpublished="Formal specification for the proof assistant Matita 0.99.2", + year="2014", + month="July", + note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" +} + @incollection{lambdadelta7, author="F. {Guidi}", title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", @@ -21,6 +32,8 @@ month="September" } +% \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + @article{lambdadelta5, author="F. {Guidi}", title="{The Formal System $\lambda\delta$}", @@ -71,7 +84,7 @@ @misc{lambdadelta1, author="F. {Guidi}", title="{lambdadelta\_1}", - howpublished="Formal specification with the proof assistant Coq 7.3.1", + howpublished="Formal specification for the proof assistant Coq 7.3.1", year="2006", month="November", note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz new file mode 100644 index 000000000..6dc4aa81c Binary files /dev/null and b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz differ diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 765dcea06..c9e6adaf6 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -23,7 +23,8 @@

-

Summary of the Specification

Summary of the Specification

Here is a numerical acount of the specification's contents and its timeline. Nodes are counted according to the "intrinsinc complexity measure" @@ -35,21 +36,21 @@ - - - + + - - - - @@ -96,7 +97,8 @@ -

Logical Structure of the Specification

Logical Structure of the Specification

The source files are grouped in planes according to the following table. Notation files covering the whole specification are provided. @@ -107,30 +109,30 @@

- - - + + - - - - - - - @@ -204,7 +206,8 @@

Physical Structure of the Specification

Physical Structure of the Specification

The source files are grouped in directories, one for each plane.

@@ -234,6 +237,6 @@

Last update: Sat, 28 Jun 2014 20:29:31 +0200

Last update: Sun, 29 Jun 2014 22:20:18 +0200

diff --git a/helm/www/lambdadelta/web/home/index2.ldw.xml b/helm/www/lambdadelta/web/home/index2.ldw.xml new file mode 100644 index 000000000..14be7fa88 --- /dev/null +++ b/helm/www/lambdadelta/web/home/index2.ldw.xml @@ -0,0 +1,39 @@ + + + + + + Foreword + + The formal system Î»Î´ (\lambda\delta) is a typed Î»-calculus aiming to support + the foundations of Mathematics that require an underlying specification language + (for example the Minimal Type Theory + and its predecessors). + + + Î»Î´ is developed in the context of the + Hypertextual Electronic Library of Mathematics + 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: + + + + Notice for the Internet Explorer user + + To view this site correctly, please select a font + with Unicode support. + For example "Lucida Sans Unicode" (it should be already installed on your system). + To change the current font follow: + "Tools" menu â "Internet Options" entry â "General" tab â "Fonts" button. + + +