From 1aca50505c3ce6c76dd7d20d00e358707caffd4a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 19 Dec 2019 17:16:44 +0100 Subject: [PATCH] updated web site + updated change log + updated site generation procedure --- helm/www/lambdadelta/Makefile | 84 ++++++------ matita/matita/contribs/lambdadelta/Makefile | 10 +- .../contribs/lambdadelta/web/changes.tbl | 121 ++++++++++++------ 3 files changed, 131 insertions(+), 84 deletions(-) diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 391b4e1f8..98fb867c7 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -1,25 +1,26 @@ SHELL := $(shell which bash) H=@ +TAGS = up-html up-html-ix up-home html html-ix home ldw ldw-ix + TAGS = www up-html up-css up-images up-download \ lint-xml index lddl install-xml \ test-html html install-html \ install-jed install-bib install-2 install-1 install-coq \ install-automath install-v install-matita \ -# LDURL = http://lambdadelta.info/ -LDURL = http://helm.cs.unibo.it/lambdadelta/ +LDWEBURL = http://helm.cs.unibo.it/lambdadelta/ SITEDIR = html -ETCDIR = etc -DOWNDIR = download -XSLTDIR = xslt -XMLDIR = xml +HTMLDIR = html/lddl SRCDIR = web/home LDDLDIR = web/lddl XHTBLDIR = bin/xhtbl INDEXDIR = bin/index -HTMLDIR = html/lddl +ETCDIR = etc +DOWNDIR = download +XSLTDIR = xslt +XMLDIR = xml JEDDIR = $(HOME)/mps/jed BIBDIR = $(HOME)/texmf/bibtex/bib CONTRIBDIR = $(ETCDIR)/lambdadelta @@ -36,10 +37,12 @@ RSTATICDIR = /projects/helm/public_html/lambda-delta/static HTMLSTAMP = $(ETCDIR)/html.stamp HTMLIXSTAMP = $(ETCDIR)/html_ix.stamp +HOMESTAMP = $(ETCDIR)/home.stamp LDWSTAMP = $(ETCDIR)/ldw.stamp LDWIXSTAMP = $(ETCDIR)/ldw_ix.stamp SITEMAP = $(XSLTDIR)/sitemap.xsl +TABLES = $(XSLTDIR)/xhtbl.xsl SLS = helena.sl automath.sl BIB = lambdadelta.bib @@ -80,35 +83,14 @@ ifeq ($(XSLT), xalan) XSLT += -indent 2 endif -XSLT += $(XSLT_PARAM) baseurl '"$(LDURL)"' $(XSLT_PARAM) date '"$(shell date -R)"' - -define HTML_TEMPLATE - HTML_$(2) = $$(SITEDIR)/$(2).html - HTMLS += $$(HTML_$(2)) - - $$(HTML_$(2)): $(1) $$(XSLS) $$(LDWEB:%=$$(XSLTDIR)/%) - @echo " XSLT $$(notdir $$<)" - $$(H)$$(XSLT) $$(XSLT_OUT) $$@ $$(XSLT_XSL) $$(XSLTDIR)/ld_web.xsl $$(XSLT_IN) $$< -endef - -ifeq ($(MAKECMDGOALS), home) - LDWS = $(shell find -L $(WEBDIRS) -name "*.ldw.xml") - TBLS = $(shell find -L $(WEBDIRS) -name "*.tbl") - XSLS = $(addprefix $(XSLTDIR)/,xhtbl.xsl $(notdir $(TBLS:%.tbl=%.xsl))) - - $(XSLS): $(TBLS) $(XHTBL) - @echo " XHTBL $(XHTBLOPTS) *.tbl" - $(H)$(XHTBL) $(XHTBLOPTS) -b $(LDURL) -O $(XSLTDIR) $(TBLS) - - $(foreach LDW,$(LDWS),$(eval $(call HTML_TEMPLATE,$(LDW),$(notdir $(LDW:%.ldw.xml=%))))) -endif +XSLT += $(XSLT_PARAM) baseurl '"$(LDWEBURL)"' $(XSLT_PARAM) date '"$(shell date -R)"' all: # UPDATE HTML LDDL ########################################################### $(ETCDIR)/html_lddl.tar.bz2: $(HTMLSTAMP) - @echo " INSTALL html" + @echo " UPDATE $(RHOMEDIR)/$(HTMLDIR)/" $(H)tar -cjf $@ $(HTMLDIR) $(H)scp $@ $(RHOMEDIR)/$(ETCDIR) $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@" @@ -118,7 +100,7 @@ up-html: $(ETCDIR)/html_lddl.tar.bz2 # UPDATE HTML IX LDDL ######################################################## $(ETCDIR)/html_lddl_ix.tar.bz2: $(HTMLIXSTAMP) - @echo " INSTALL html-ix" + @echo " UPDATE $(RHOMEDIR)/$(HTMLDIR)/*/index.html" $(H)tar -cjf $@ `find $(HTMLDIR) -name index.html` $(H)scp $@ $(RHOMEDIR)/$(ETCDIR) $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@" @@ -127,14 +109,16 @@ up-html-ix: $(ETCDIR)/html_lddl_ix.tar.bz2 # UPDATE HTML HOME ########################################################### -up-home: - @echo " UPDATE $(RHOMEDIR)/html/" - $(H)scp -q html/*.html $(RHOMEDIR)/html/ +up-home: $(HOMESTAMP) + @echo " UPDATE $(RHOMEDIR)/$(SITEDIR)/" + $(H)scp -q html/*.html $(RHOMEDIR)/$(SITEDIR)/ # GENERATE HTML LDDL ######################################################### -$(HTMLSTAMP): $(LDWSTAMP) $(SITEMAP) - $(H)for LDW in `find $(LDDLDIR) -name *.ldw.xml`; do \ +$(HTMLSTAMP): LDWS = `find $(LDDLDIR) -name *.ldw.xml` + +$(HTMLSTAMP): $(LDWSTAMP) $(SITEMAP) $(LDWEB:%=$(XSLTDIR)/%) + $(H)for LDW in $(LDWS); do \ TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \ echo " XSLT $$LDW"; \ mkdir -p $${HTML%/*}; \ @@ -147,8 +131,10 @@ html: $(HTMLSTAMP) # GENERATE HTML IX LDDL ###################################################### -$(HTMLIXSTAMP): $(LDWIXSTAMP) $(SITEMAP) - $(H)for LDW in `find $(LDDLDIR) -name index.ldw.xml`; do \ +$(HTMLIXSTAMP): LDWS = `find $(LDDLDIR) -name index.ldw.xml` + +$(HTMLIXSTAMP): $(LDWIXSTAMP) $(SITEMAP) $(LDWEB:%=$(XSLTDIR)/%) + $(H)for LDW in $(LDWS); do \ TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \ echo " XSLT $$LDW"; \ mkdir -p $${HTML%/*}; \ @@ -160,7 +146,25 @@ html-ix: $(HTMLIXSTAMP) # GENERATE HTML HOME ######################################################### -home: $(HTMLS) $(TBLS) $(XHTBL) +$(HOMESTAMP): LDWS = `find -L $(WEBDIRS) -name "*.ldw.xml"` + +$(HOMESTAMP): $(LDWS) $(TABLES) $(LDWEB:%=$(XSLTDIR)/%) + $(H)for LDW in $(LDWS); do \ + TMP=$${LDW##*/};HTML=$${TMP/ldw.xml/html}; \ + echo " XSLT $$LDW"; \ + $(XSLT) $(XSLT_OUT) $(SITEDIR)/$$HTML $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $$LDW; \ + done + $(H)touch $@ + +home: $(HOMESTAMP) + +# GENERATE XSL ############################################################### + +$(TABLES) $(SITEMAP): TBLS = `find -L $(WEBDIRS) -name "*.tbl"` + +$(TABLES) $(SITEMAP): $(TBLS) $(XHTBL) + @echo " XHTBL $(XHTBLOPTS) *.tbl" + $(H)$(XHTBL) $(XHTBLOPTS) -b $(LDWEBURL) -O $(XSLTDIR) $(TBLS) # GENERATE LDW LDDL ########################################################## @@ -253,7 +257,5 @@ up-download: # @echo " XSLT $@" # $(H)mkdir -p $(LDDLDIR)/$(@D) # $(H)$(XSLT) --novalid $(XSLT_OUT) $(LDDLDIR)/$@.ldw.xml $(XSLT_XSL) $(XSLTDIR)/lddl.xsl $(XSLT_IN) $(XMLDIR)/$@.xml -# $(H)mkdir -p $(HTMLDIR)/$(@D) -# $(H)$(XSLT) $(XSLT_OUT) $(HTMLDIR)/$@.html $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $(LDDLDIR)/$@.ldw.xml .PHONY: $(TAGS) diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index ff1ebeeef..4438f07b5 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -30,7 +30,7 @@ CONTRIB := lambdadelta_2B WWW := ../../../../helm/www/lambdadelta TAGS := all xoa xoa2 orig elim deps top leaf stats tbls odeps trim contrib clean \ - www up-html + home up-home PACKAGES := ground_2 static_2 basic_2 apps_2 alpha_1 XPACKAGES := ground_2 static_2 basic_2 @@ -270,13 +270,13 @@ clean: # www ###################################################################### -www: - $(H)$(MAKE) --no-print-directory -C $(WWW) www +home: + $(H)$(MAKE) --no-print-directory -C $(WWW) home # www ###################################################################### -up-html: - $(H)$(MAKE) --no-print-directory -C $(WWW) up-html +up-home: + $(H)$(MAKE) --no-print-directory -C $(WWW) up-home ############################################################################## diff --git a/matita/matita/contribs/lambdadelta/web/changes.tbl b/matita/matita/contribs/lambdadelta/web/changes.tbl index bf985679d..42002da82 100644 --- a/matita/matita/contribs/lambdadelta/web/changes.tbl +++ b/matita/matita/contribs/lambdadelta/web/changes.tbl @@ -12,23 +12,34 @@ table { { "@" "" "@" } { "+" "-" "*" } { "type assignment (terms)" - "stratified higher validity (terms) removed" + "higher validity (terms) removed" "primitive validity (terms)" } ] [ [{ "equivalences" * }] - { "" "" "" "" } - { "+" "+" "+" "-" } - { "equivalence for full rt-reduction (terms)" - "equivalence for whd rt-reduction (terms)" - "equivalence for full rt-reduction (terms, referred lenvs, closures)" - "syntactic equivalence (closures) removed" + { "" "" "" "" "" } + { "+" "+" "+" "+" "-" } + { "equivalence for whd rt-reduction (terms)" + "equivalence for full rt-reduction (terms, items, referred lenvs, referred closures)" + "equivalence up to exclusion binders (selected lenvs)" + "syntactic equivalence (items)" + "syntactic equivalence (selected closures) removed" } ] [ [{ "partial orders" * }] + { "" "" "" "" "" } + { "+" "+" "+" "+" "+" } + { "properties with inclusion (hereditarily free variables)" + "inclusion (hereditarily free variables)" + "inclusion (applicability)" + "switch in primitive order relations (closures) to enable the exclusion binder" + "simple weight (items, genvs)" + } + ] + [ [{ "reducibility" * }] { "" } - { "+" } - { "switch in primitive order relations for closures to enable the exclusion binder" + { "*" } + { "abatract Tait's candidates with 6 postulates" } ] [ [{ "normal form predicates" * }] @@ -47,25 +58,57 @@ table { { "zero or more refs (terms) removed" } ] - [ [{ "relocation" * }] - { "" "" "" "" } - { "-" "*" "-" "*" } - { "basic slicing (lenvs) removed" + [ [{ "relocation and slicing" * }] + { "" "" "" "" "" "" } + { "+" "-" "*" "-" "+" "*" } + { "properties with abstract relocation (terms/items)" + "basic slicing (lenvs) removed" "primitive finite slicing (lenvs)" - "basic relocation (lists of terms) removed" + "basic relocation (terms, lists of terms) removed" + "primitive finite relocation (items)" "primitive finite relocation (terms, lists of terms)" } ] [ [{ "free varibles" * }] - { "" } - { "+" } - { "union (referred lenvs) removed" + { "" "" } + { "+" "-" } + { "refinement for hereditarily free variables (lenvs)" + "union (referred lenvs) removed" + } + ] + [ [{ "helpers" * }] + { "" "" "" } + { "+" "+" "+" } + { "append (restricted closures) wrong on excluded entries" + "length (genvs)" + "abstract properties with append (lenvs)" + } + ] + [ [{ "extension" * }] + { "" "" "" "" "" } + { "+" "+" "+" "+" "+" } + { "properties with iterated extension (referred lenvs)" + "iterated for 3-relations (referred lenvs)" + "abstract properties with extension (selected lenvs)" + "for 3-relations (selected lenvs)" + "for 2-relations and 3-relations (items)" } ] [ [{ "syntax" * }] - { "@" } - { "+" } - { "exclusion binder for lenvs" + { "@" "" } + { "+" "+" } + { "exclusion binder (lenvs)" + "bonding items (lenvs)" + } + ] + [ [{ "parameters" * }] + { "" "" "@" "" "@" } + { "+" "+" "+" "+" "*" } + { "concrete instances (applicability)" + "abstract properties (applicability)" + "abstract applicability condition" + "sort hierarchy properties including strict monotonicity condition based on non-negative integers" + "abstract sort hierarchy without properties" } ] [ [{ "ground" * }] @@ -96,24 +139,26 @@ table { } ] [ [{ "equivalences" * }] - { "@" "" "@" "" "" "" } - { "+" "+" "-" "-" "-" "+" } + { "@" "" "@" "" "" "" "" } + { "+" "+" "-" "-" "-" "+" "+" } { "primitive decomposed rt-equivalence (terms)" "single-step context-sensitive r-eqivalence (terms)" "primitive context-sensitive r-eqivalence (terms) removed" "context-free r-eqivalence (terms) removed" "level equivalence (binary arities) removed" - "syntactic equivalence (selected lenvs, referred lenvs, selected closures)" + "properties with syntactic equivalence (referred lenvs)" + "syntactic equivalence (selected lenvs, referred lenvs, referred closures)" } ] [ [{ "partial orders" * }] - { "" "" "" "" "" "" "" } - { "+" "*" "+" "-" "-" "-" "-" } + { "" "" "" "" "" "" "" "" } + { "+" "*" "+" "-" "-" "-" "-" "-" } { "big-tree order relations (closures)" "primitive order relations for closures" "simple weight (restricted closures)" + "order relation (lenvs) based on look-up removed" "order relation (lists of terms) based on lengths removed" - "order relations (binary arities) based on weights removed" + "order relations (terms, lenvs, binary arities) based on weights removed" "simple weights (binary arities) removed" "complex weight (terms) removed" } @@ -136,7 +181,7 @@ table { { "+" "+" "+" "+" "+" "-" "+" "+" "+" } { "evaluation for full rt-reduction (terms)" "normal form for full rt-reduction (terms)" - "irreducible forms for fulld rt-reduction (terms)" + "irreducible forms for full rt-reduction (terms)" "reducible forms for full rt-reduction (terms)" "evaluation for reduction (terms)" "normal form for reduction (lists of terms) removed" @@ -169,7 +214,7 @@ table { } ] [ [{ "degree" * }] - { "@" "" "@" "" } + { "" "@" "" "@" } { "+" "+" "+" "+" } { "refinement for degree (lenvs)" "degree assignment (terms)" @@ -204,7 +249,7 @@ table { "refinement (selected lenvs)" "append (lenvs)" "left cons (lenvs) removed" - "flat construction clear (lenvs) removed" + "flat entry clear (lenvs) removed" "sort extraction (lenvs) removed" "context predicate (terms) removed" "neutral predicate (terms)" @@ -232,7 +277,7 @@ table { ] [ [{ "parameters" * }] { "" "" } - { "+" "-"} + { "+" "-" } { "concrete sort hierarchies" "iterated next function (sort hierarchy) removed" } @@ -270,9 +315,10 @@ table { } ] [ [{ "partial orders" * }] - { "" "" "" "" } - { "+" "+" "+" "+" } - { "order relation (specialized lists of terms) based on lengths" + { "" "" "" "" "" } + { "+" "+" "+" "+" "+" } + { "order relation (lenvs) based on look-up" + "order relation (specialized lists of terms) based on lengths" "order relations (terms, lenvs, closures, binary arities) based on weights" "simple weights (terms, lenvs, closures, binary arities)" "complex weight (terms)" @@ -293,7 +339,7 @@ table { [ [{ "normal form predicates" * }] { "" } { "+" } - { "normal form for context-sensitive reduction (terms, specialized lists of terms)" + { "normal form for reduction (terms, specialized lists of terms)" } ] [ [{ "reduction and type synthesis" * }] @@ -316,10 +362,9 @@ table { } ] [ [{ "relocation and slicing" * }] - { "" "" "" "" "" "" "" "" } - { "+" "+" "+" "+" "+" "+" "+" "+" } - { "order relation (lenvs) based on look-up" - "look-up predicate (lenvs)" + { "" "" "" "" "" "" "" } + { "+" "+" "+" "+" "+" "+" "+" } + { "look-up predicate (lenvs)" "finite slicing (lenvs)" "basic slicing (lenvs)" "finite relocation (terms, specialized lists of terms)" -- 2.39.2