X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2FMakefile;h=073dc33a2b640d6b971c771f546e7c4c6503fe3f;hp=6bb4350829abcfefd3ce85cf91b5d5b89cbe26e5;hb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;hpb=be2870b722324a1813ac9e72ebcb2cda6c8733d7

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index 6bb435082..073dc33a2 100644
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -11,7 +11,6 @@ XOA          := xoa.native
 XOA_OPTS     := ../../matita.conf.xml $(XOA_CONF)
 
 XOA2_CONF    := ground_2/xoa2.conf.xml
-XOA2_TARGETS := ground_2/notation/xoa/notation2.ma ground_2/xoa/xoa2.ma
 XOA2_OPTS    := ../../matita.conf.xml $(XOA2_CONF)
 
 DEP_INPUT    := .depend
@@ -28,9 +27,12 @@ ORIGS        := basic_2/basic_1.orig
 
 CONTRIB      := lambdadelta_2
 
-TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib
+WWW          := ../../../../helm/www/lambdadelta
 
-PACKAGES  := ground_2 basic_2 apps_2 alpha_1
+TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean \
+        www up-html
+
+PACKAGES  := ground_2 basic_2 static_2 apps_2 alpha_1
 XPACKAGES := ground_2 basic_2
 
 LDWS := $(shell find -name "*.ldw.xml")
@@ -67,15 +69,13 @@ xoa: $(XOA_TARGETS)
 
 $(XOA_TARGETS): $(XOA_CONF)
 	@echo "  EXEC $(XOA) $(XOA_CONF)"
-	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_OPTS)
+	$(H)$(XOA_DIR)/$(XOA) $(XOA_OPTS)
 
 # xoa2 #######################################################################
 
-xoa2: $(XOA2_TARGETS)
-
-$(XOA2_TARGETS): $(XOA2_CONF)
+xoa2: $(XOA2_CONF)
 	@echo "  EXEC $(XOA) $(XOA2_CONF)"
-	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA2_OPTS)
+	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) -s $(XOA2_OPTS)
 
 # elim #######################################################################
 
@@ -192,7 +192,9 @@ define SUMMARY_TEMPLATE
   $$(SUM_$(1)): C0 = $$(shell cat $(1)/$(1)_probe.txt)
   $$(SUM_$(1)): S1 = $$(word 1, $$(C0))
   $$(SUM_$(1)): S2 = $$(word 2, $$(C0))
+  $$(SUM_$(1)): S3 = $$(word 3, $$(C0))
   $$(SUM_$(1)): S4 = $$(word 4, $$(C0))
+  $$(SUM_$(1)): S5 = $$(shell printf "%.1f" `echo "scale=2;$$(S4)/$$(S2)"|bc`)
   $$(SUM_$(1)): C1 = $$(word 5, $$(C0))
   $$(SUM_$(1)): C2 = $$(word 7, $$(C0))
   $$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc)
@@ -200,32 +202,32 @@ define SUMMARY_TEMPLATE
   $$(SUM_$(1)): P2 = $$(word 9, $$(C0))
   $$(SUM_$(1)): P3 = $$(shell echo "$$(P1)+$$(P2)"|bc)
 
-  $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt
+  $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt Makefile
 	@printf '  SUMMARY $(1)\n'
-	@printf 'name "$$(basename $$(@F))"\n\n'                  >  $$@
-	@printf 'table {\n'                                       >> $$@
-	@printf '   class "gray"  [ "category"\n'                 >> $$@
-	@printf '      [ "objects" * ]\n'                         >> $$@
-	@printf '   ]\n'                                          >> $$@
-	@printf '   class "water" [ "sizes"\n'                    >> $$@
-	@printf '      [ "files"      "$$(S1)" ]\n'               >> $$@
-	@printf '      [ "characters" "$$(S2)" ]\n'               >> $$@
-	@printf '      [ "nodes"      "$$(S4)" ]\n'               >> $$@
-	@printf '   ]\n'                                          >> $$@	
-	@printf '   class "green" [ "propositions"\n'             >> $$@
-	@printf '      [ "theorems" "$$(P1)" ]\n'                 >> $$@
-	@printf '      [ "lemmas"   "$$(P2)" ]\n'                 >> $$@
-	@printf '      [ "total"    "$$(P3)" ]\n'                 >> $$@
-	@printf '   ]\n'                                          >> $$@
-	@printf '   class "grass" [ "concepts"\n'                 >> $$@
-	@printf '      [ "declared" "$$(C1)" ]\n'                 >> $$@
-	@printf '      [ "defined"  "$$(C2)" ]\n'                 >> $$@
-	@printf '      [ "total"    "$$(C3)" ]\n'                 >> $$@
-	@printf '   ]\n'                                          >> $$@
-	@printf '}\n\n'                                           >> $$@
-	@printf 'class "capitalize italic" { 0 }\n\n'             >> $$@
-	@printf 'class "italic"            { 1 } { 3 } { 5 }\n\n' >> $$@
-	@printf 'class "right italic"      { 2 } { 4 } { 6 }\n'   >> $$@
+	@printf 'name "$$(basename $$(@F))"\n\n'                        >  $$@
+	@printf 'table {\n'                                             >> $$@
+	@printf '   class "gray"  [ "category"\n'                       >> $$@
+	@printf '      [ "units" * ]\n'                                 >> $$@
+	@printf '   ]\n'                                                >> $$@
+	@printf '   class "water" [ "sizes"\n'                          >> $$@
+	@printf '      [ "characters (files)"    "$$(S2) ($$(S1))" ]\n' >> $$@
+	@printf '      [ "nodes (objects)"       "$$(S4) ($$(S3))" ]\n' >> $$@
+	@printf '      [ "intrinsic loss factor" "$$(S5)" ]\n'          >> $$@
+	@printf '   ]\n'                                                >> $$@	
+	@printf '   class "green" [ "propositions"\n'                   >> $$@
+	@printf '      [ "theorems" "$$(P1)" ]\n'                       >> $$@
+	@printf '      [ "lemmas"   "$$(P2)" ]\n'                       >> $$@
+	@printf '      [ "total"    "$$(P3)" ]\n'                       >> $$@
+	@printf '   ]\n'                                                >> $$@
+	@printf '   class "grass" [ "concepts"\n'                       >> $$@
+	@printf '      [ "declared" "$$(C1)" ]\n'                       >> $$@
+	@printf '      [ "defined"  "$$(C2)" ]\n'                       >> $$@
+	@printf '      [ "total"    "$$(C3)" ]\n'                       >> $$@
+	@printf '   ]\n'                                                >> $$@
+	@printf '}\n\n'                                                 >> $$@
+	@printf 'class "capitalize italic" { 0 }\n\n'                   >> $$@
+	@printf 'class "italic"            { 1 } { 3 } { 5 }\n\n'       >> $$@
+	@printf 'class "right italic"      { 2 } { 4 } { 6 }\n'         >> $$@
 
 .PHONY: $$(SUM_$(1))
 endef
@@ -252,6 +254,21 @@ contrib:
 	@echo "  TAR -czf $(CONTRIB).tar.gz root $(XPACKAGES)"
 	$(H)tar -czf $(CONTRIB).tar.gz root $(XMAS)
 
+# clean ######################################################################
+
+clean:
+	$(H)$(RM) `find -name "*~" -type f -print`
+
+# www ######################################################################
+
+www:
+	$(H)$(MAKE) --no-print-directory -C $(WWW) www
+
+# www ######################################################################
+
+up-html:
+	$(H)$(MAKE) --no-print-directory -C $(WWW) up-html
+
 ##############################################################################
 
 .PHONY: $(TAGS)