From: Ferruccio Guidi Date: Thu, 25 Dec 2014 15:38:27 +0000 (+0000) Subject: lddl update with the disambiguated "grundlagen" X-Git-Tag: make_still_working~773 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68b5af5ca8f1e7f98485b92692b3dcb1ae240d19;p=helm.git lddl update with the disambiguated "grundlagen" --- diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 07ecd4e4e..e35c1c85a 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -10,7 +10,8 @@ KEEP = README CLEAN = etc/log.txt etc/profile.txt -TAGS = test-si-fast test-si test-si-matita test profile xml xml-v3 matita matitac +TAGS = test-si-fast test-si test-si-matita test profile \ + xml-si xml-si-v3 xml xml-v3 matita matitac include Makefile.common @@ -50,13 +51,21 @@ profile: $(MAIN).opt etc $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -o -q $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt +xml-si: $(MAIN).opt etc + @echo " HELENA -l -o -s 1 -x $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -x $(INPUT) > etc/log.txt + +xml-si-v3: $(MAIN).opt etc + @echo " HELENA -l -o -s 2 -x $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -x $(INPUT) > etc/log.txt + xml: $(MAIN).opt etc @echo " HELENA -l -s 1 -x $(INPUT)" $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 1 -x $(INPUT) > etc/log.txt xml-v3: $(MAIN).opt etc @echo " HELENA -l -s 2 -x $(INPUT)" - $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 3 -x $(INPUT) > etc/log.txt + $(H)./$(MAIN).opt -l -o $(INPUT) -X -O $(XMLDIR) -T 1 -l -s 2 -x $(INPUT) > etc/log.txt matita: matita/$(MA) @echo " MATITA $(MA)" diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index 3a394c5b7..227a524e2 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -55,10 +55,14 @@ let ma_preamble = ref "" (* location of grafite preamble file *) let alpha = ref "" (* prefix of numeric identifiers *) -let kernel_id () = match !kernel with - | V4 -> "" - | V3 -> "V3" - | V0 -> "V0" +let kernel_id () = + let id = match !kernel with + | V4 -> "Environment" + | V3 -> "Environment_V3" + | V0 -> "Environment_V0" + in + let si = if !si then "_si" else "" in + id ^ si let get_baseuri () = String.concat "/" ["ld:"; kernel_id (); !cover; "" ] diff --git a/helm/software/helena/src/xml/xmlLibrary.ml b/helm/software/helena/src/xml/xmlLibrary.ml index d51af0bfb..584dc776a 100644 --- a/helm/software/helena/src/xml/xmlLibrary.ml +++ b/helm/software/helena/src/xml/xmlLibrary.ml @@ -133,7 +133,8 @@ let export_entity pp_term (ra, na, u, b) = | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v) | E.Void -> assert false in + let opts = if !G.si then "si" else "" in let shp = H.string_of_graph () in - let attrs = [xmlns; "hierarchy", shp] in + let attrs = [xmlns; "hierarchy", shp; "options", opts] in tag obj_root attrs ~contents out 0; close_out och diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 219255375..9050909b2 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Tue, 04 Nov 2014 16:28:52 +0100
+
Last update: Wed, 24 Dec 2014 22:58:52 +0100
diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index c583563f0..b8b2996ad 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -23,18 +23,20 @@ WEBDIRS = $(SRCDIR) $(ETCDIR) REMOTE = helm.cs.unibo.it RDIR = /projects/helm/public_html/lambdadelta -RXMLDIR = $(REMOTE):$(RDIR)/xml -RHTMLDIR = $(REMOTE):$(RDIR)/static/lddl +RHOMEDIR = $(REMOTE):$(RDIR) +RXMLDIR = $(RHOMEDIR)/xml +RHTMLDIR = $(RHOMEDIR)/static/lddl +RDOWNDIR = $(RHOMEDIR)/download SLS = helena.sl automath.sl BIB = lambdadelta.bib CONTRIB = lambdadelta_2.tar.gz -XMLS = grundlagen_2/l/not.ld.xml \ - grundlagen_2/l/et.ld.xml \ - grundlagen_2/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \ - grundlagen_2/l/e/pairis1.ld.xml \ - grundlagen_2/l/e/st/eq/landau/n/327/t25.ld.xml \ +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 @@ -93,13 +95,16 @@ $(ETCDIR)/make-html.sh $(XMLDIR)/index.txt index: $(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) -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" + +# $(H)scp -r $(XMLDIR) $(RXMLDIR) test-html: @$(MAKE) --no-print-directory $(XMLS:%.xml=%) @@ -126,7 +131,7 @@ install-contrib: $(CONTRIB:%=$(CONTRIBDIR)/%) $(H)scp $< $(DOWNDIR) up: - @echo " UPDATE $(REMOTE):$(RDIR)" + @echo " UPDATE $(RHOMEDIR)" $(H)ssh $(REMOTE) "svn up $(RDIR)" %.ld: diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 31b4d9c92..5184a4d12 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -142,29 +142,29 @@ sizes files - 4 + 14 characters - 68581 + 6787 nodes - 3637 + 10070 propositions theorems 2 lemmas - 1 + 4 total - 3 + 6 concepts declared - 3 + 6 defined - 9 + 11 total - 12 + 17 @@ -250,6 +250,6 @@

-
Last update: Tue, 04 Nov 2014 16:28:52 +0100
+
Last update: Wed, 24 Dec 2014 22:58:52 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index e67e7d200..353b1c74e 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -126,7 +126,7 @@ characters 433402 nodes - 1874774 + 1874778 propositions @@ -1366,6 +1366,6 @@

-
Last update: Tue, 04 Nov 2014 16:28:52 +0100
+
Last update: Wed, 24 Dec 2014 22:58:52 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 38d99b003..8d7d6b753 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -358,6 +358,6 @@

-
Last update: Tue, 04 Nov 2014 16:28:51 +0100
+
Last update: Wed, 24 Dec 2014 22:58:52 +0100
diff --git a/helm/www/lambdadelta/download/lddl.tar.bz2 b/helm/www/lambdadelta/download/lddl.tar.bz2 index 06b341d98..0237443ce 100644 Binary files a/helm/www/lambdadelta/download/lddl.tar.bz2 and b/helm/www/lambdadelta/download/lddl.tar.bz2 differ diff --git a/helm/www/lambdadelta/etc/exclude.txt b/helm/www/lambdadelta/etc/exclude.txt new file mode 100644 index 000000000..c9a35c984 --- /dev/null +++ b/helm/www/lambdadelta/etc/exclude.txt @@ -0,0 +1 @@ +xml/.svn diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index e5218996f..7f5ada5fd 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -123,7 +123,7 @@ files 30 characters - 68581 + 46649 nodes 62380 @@ -288,6 +288,6 @@

-
Last update: Tue, 04 Nov 2014 16:28:52 +0100
+
Last update: Wed, 24 Dec 2014 22:58:52 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 9b819674c..2881bbd76 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -111,8 +111,8 @@
  • Access: static pages (updated 2012-10), - data set (updated 2012-10), - HELM server URL (updated 2012-10). + data set (updated 2014-12), + HELM server URL (updated 2014-12).