X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2FMakefile;h=df4a4b51942408d74a716fc85918d5464706eb97;hp=0da13bb383983d363cceae09549166c85a496ba3;hb=7bb7028a9aafcfd5c6570f4ad5ca472f19691bfc;hpb=add1600e1ceef0f1c7e07a4d13c60edd7a3ea367 diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index 0da13bb38..df4a4b519 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -1,61 +1,90 @@ +SHELL := $(shell which bash) H=@ -TAGS = www up \ +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 \ - -LDURL = http://lambdadelta.info/ -LDDLURL = $(LDURL)static/lddl - -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 + 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/ + +SITEDIR = html +ETCDIR = etc +DOWNDIR = download +XSLTDIR = xslt +XMLDIR = xml +SRCDIR = web/home +LDDLDIR = web/lddl +XHTBLDIR = bin/xhtbl +INDEXDIR = bin/index +HTMLDIR = html/lddl +JEDDIR = $(HOME)/mps/jed +BIBDIR = $(HOME)/texmf/bibtex/bib +CONTRIBDIR = $(ETCDIR)/lambdadelta +HELENADIR = ../../software/helena WEBDIRS = $(SRCDIR) $(ETCDIR) REMOTE = helm.cs.unibo.it RDIR = /projects/helm/public_html/lambdadelta -RXMLDIR = $(REMOTE):$(RDIR)/xml -RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl - -SLS = helena.sl automath.sl -BIB = lambdadelta.bib - -XMLS = brg_si/grundlagen/l/not.ld.xml \ - brg_si/grundlagen/l/et.ld.xml \ - brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - brg_si/grundlagen/l/e/pairis1.ld.xml \ - brg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ - crg_si/grundlagen/l/not.ld.xml \ - crg_si/grundlagen/l/et.ld.xml \ - crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - crg_si/grundlagen/l/e/pairis1.ld.xml \ - crg_si/grundlagen/l/e/st/eq/landau/n/327/t25.ld.xml \ - brg_si/grundlagen/ccs.ldc.xml - -LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl +RHOMEDIR = $(REMOTE):$(RDIR) +RXMLDIR = $(RHOMEDIR)/xml +RDOWNDIR = $(RHOMEDIR)/download +RSTATICDIR = /projects/helm/public_html/lambda-delta/static + +DLHTMLSTAMP = $(ETCDIR)/lddl_html.stamp +DLHTMLIXSTAMP = $(ETCDIR)/lddl_html_ix.stamp + +SLS = helena.sl automath.sl +BIB = lambdadelta.bib +CONTRIB = lambdadelta_2.tar.gz + +XMLS = Environment/grundlagen_2/l/not.ld.xml \ + Environment/grundlagen_2/l/et.ld.xml \ + Environment/grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ + Environment/grundlagen_2/l/e/pairis1.ld.xml \ + Environment/grundlagen_2/l/e/st/eq/landau/n/327/t25.ld.xml \ + +LDWEB = ld_web.xsl ld_web_root.xsl ld_web_library.xsl ld_web_ebnf.xsl + +AUTOMATH = examples/automath/grundlagen_2.aut +COQ = coq/grundlagen_2.v + +MATITA = matita/root matita/grundlagen_2.ma XMLLINT = xmllint --noout XSLT = xsltproc XHTBL = $(XHTBLDIR)/xhtbl.native +INDEX = $(INDEXDIR)/index.native -%.html: BASEURL = --stringparam baseurl $(LDURL) +XHTBLOPTS = + +ifeq ($(XSLT), xsltproc) + XSLT_PARAM := --param + XSLT_OUT := -o + XSLT_XSL := + XSLT_IN := +endif + +ifeq ($(XSLT), xalan) + XSLT_PARAM := -param + XSLT_OUT := -out + XSLT_XSL := -xsl + XSLT_IN := -in + XSLT += -indent 2 +endif + +XSLT += $(XSLT_PARAM) baseurl '"$(LDURL)"' $(XSLT_PARAM) date '"$(shell date -R)"' define HTML_TEMPLATE - HTML_$(2) = $$(HOMEDIR)/$(2).html + HTML_$(2) = $$(SITEDIR)/$(2).html HTMLS += $$(HTML_$(2)) $$(HTML_$(2)): $(1) $$(XSLS) $$(LDWEB:%=$$(XSLTDIR)/%) @echo " XSLT $$(notdir $$<)" - $$(H)$$(XSLT) -o $$@ $$(BASEURL) $$(XSLTDIR)/ld_web.xsl $$< + $$(H)$$(XSLT) $$(XSLT_OUT) $$@ $$(XSLT_XSL) $$(XSLTDIR)/ld_web.xsl $$(XSLT_IN) $$< endef ifeq ($(MAKECMDGOALS), www) @@ -64,43 +93,78 @@ ifeq ($(MAKECMDGOALS), www) XSLS = $(addprefix $(XSLTDIR)/,xhtbl.xsl $(notdir $(TBLS:%.tbl=%.xsl))) $(XSLS): $(TBLS) $(XHTBL) - @echo " XHTBL *.tbl" - $(H)$(XHTBL) -O $(XSLTDIR) $(TBLS) + @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 -all: www +all: -www: $(HTMLS) +www: $(HTMLS) $(TBLS) $(XHTBL) lint-xml: $(XMLS:%=$(XMLDIR)/%) @echo XMLLINT --valid - $(H)$(XMLLINT) --valid $^ + $(H)$(XMLLINT) --valid $^ -$(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index: +$(ETCDIR)/make_html.sh $(XMLDIR)/index.txt index: @echo " GENERATE INDEXES" $(H)find $(XMLDIR) -name "*.ld.xml" | sed s/.xml//g | sed s/xml/ld:/g > $(XMLDIR)/index.txt $(H)sed "s/^/make --no-print-directory /" $(XMLDIR)/index.txt | sed s.ld:/.. > $(ETCDIR)/make_html.sh -lddl: $(ETCDIR)/exclude.txt index +$(DOWNDIR)/lddl.tar.bz2 lddl: $(ETCDIR)/exclude.txt $(XMLDIR)/index.txt @echo " GENERATE lddl.tar.bz2" - $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR) + $(H)tar -cjf $(DOWNDIR)/lddl.tar.bz2 -X $< $(XMLDIR) -install-xml: $(XMLDIR)/index.txt +install-xml: $(DOWNDIR)/lddl.tar.bz2 @echo " INSTALL xml" - $(H)scp -r $< $(XMLDIR)/brg_si/ $(XMLDIR)/crg_si/ $(RXMLDIR) + $(H)scp $^ $(RDOWNDIR) + $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf download/lddl.tar.bz2" test-html: @$(MAKE) --no-print-directory $(XMLS:%.xml=%) html: $(ETCDIR)/make_html.sh @echo " MAKE */*.ld" - $(H). $< +# $(H). $< + $(H)$(INDEX) -i $(LDDLDIR) -o $(HTMLDIR) . + +test: $(DLHTMLIXSTAMP) + +$(DLHTMLSTAMP): + $(H)for LDW in `find $(LDDLDIR) -name *.ldw.xml`; do \ + TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \ + echo " XSLT $$LDW"; \ + mkdir -p $${HTML%/*}; \ + $(XSLT) $(XSLT_OUT) $$HTML $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $$LDW; \ + done + $(H)touch $@ + $(H)touch $(DLHTMLIXSTAMP) + +$(DLHTMLIXSTAMP): + $(H)for LDW in `find $(LDDLDIR) -name index.ldw.xml`; do \ + TMP=$${LDW/web/html};HTML=$${TMP/ldw.xml/html}; \ + echo " XSLT $$LDW"; \ + mkdir -p $${HTML%/*}; \ + $(XSLT) $(XSLT_OUT) $$HTML $(XSLT_XSL) $(XSLTDIR)/ld_web.xsl $(XSLT_IN) $$LDW; \ + done + $(H)touch $@ + +install-html: $(ETCDIR)/html_lddl.tar.bz2 + +$(ETCDIR)/html_lddl.tar.bz2: + @echo " INSTALL html" + $(H)tar -cjf $@ $(HTMLDIR) + $(H)scp $@ $(RHOMEDIR)/$(ETCDIR) + $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@" + +install-html-ix: $(ETCDIR)/html_lddl_ix.tar.bz2 -install-html: $(ETCDIR)/make_html.sh +$(ETCDIR)/html_lddl_ix.tar.bz2: @echo " INSTALL html" - $(H)scp -r $(HTMLDIR)/* $(RHTMLDIR) +# $(H)tar -cjf $@ `find $(HTMLDIR) -name index.html` + $(H)scp $@ $(RHOMEDIR)/$(ETCDIR) + $(H)ssh $(REMOTE) "cd $(RDIR) && tar -xjf $@" install-jed: $(SLS:%=$(JEDDIR)/%) @echo " INSTALL $(SLS)" @@ -110,18 +174,52 @@ install-bib: $(BIB:%=$(BIBDIR)/%) @echo " INSTALL $(BIB)" $(H)scp $< $(DOWNDIR) $(H)scp $< $(DOWNDIR)/$(BIB:%.bib=%.txt) -up: - @echo " UPDATE $(REMOTE):$(RDIR)" - $(H)ssh $(REMOTE) "svn up $(RDIR)" -%.ld: BASEURL = --stringparam baseurl $(LDDLURL) +install-2: $(CONTRIB:%=$(CONTRIBDIR)/%) + @echo " INSTALL $(CONTRIB)" + $(H)scp $< $(DOWNDIR) + +install-automath: $(HELENADIR)/$(AUTOMATH) + @echo " INSTALL $(notdir $<)" + $(H)scp $< $(DOWNDIR) + +install-matita: $(MATITA:%=$(HELENADIR)/%) + @echo " INSTALL matita" + $(H)tar -C $(HELENADIR) -cjf $(DOWNDIR)/grundlagen_2.tar.bz2 $(MATITA) + +install-1: etc/coq/ld_731/contrib/lambdadelta.tar.gz + @echo " INSTALL $<" + $(H)scp $< $(DOWNDIR)/lambdadelta_1.tar.gz + +install-coq: + @echo " INSTALL coq" + $(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 $<)" + $(H)scp $< $(DOWNDIR) + +up-html: + @echo " UPDATE $(RHOMEDIR)/html/" + $(H)scp -q html/*.html $(RHOMEDIR)/html/ + +up-css: + @echo " UPDATE $(RHOMEDIR)/css/" + $(H)scp -q -r css $(RHOMEDIR) + +up-images: + @echo " UPDATE $(RHOMEDIR)/images/" + $(H)scp -q -r images $(RHOMEDIR) + +up-download: + @echo " UPDATE $(RHOMEDIR)/download/" + $(H)scp -q -r download $(RHOMEDIR) %.ld: @echo " XSLT $@" - $(H)mkdir -p $(HTMLDIR)/$(@D) - $(H)$(XSLT) -o $(HTMLDIR)/$@.html $(BASEURL) $(XSLTDIR)/lddl.xsl $(XMLDIR)/$@.xml - -%.ldc: - @echo " SKIP $@" +# $(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)