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
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
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 $@"
# 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 $@"
# 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%/*}; \
# 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%/*}; \
# 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 ##########################################################
# @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)
{ "@" "" "@" }
{ "+" "-" "*" }
{ "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" * }]
{ "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" * }]
}
]
[ [{ "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"
}
{ "+" "+" "+" "+" "+" "-" "+" "+" "+" }
{ "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"
}
]
[ [{ "degree" * }]
- { "@" "" "@" "" }
+ { "" "@" "" "@" }
{ "+" "+" "+" "+" }
{ "refinement for degree (lenvs)"
"degree assignment (terms)"
"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)"
]
[ [{ "parameters" * }]
{ "" "" }
- { "+" "-"}
+ { "+" "-" }
{ "concrete sort hierarchies"
"iterated next function (sort hierarchy) removed"
}
}
]
[ [{ "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)"
[ [{ "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" * }]
}
]
[ [{ "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)"
projects / helm.git / commitdiff