TRIM := sed "s/ \\+$$//"
-XOA_CONF := ground_2/xoa.conf.xml
-XOA_TARGETS := ground_2/notation/xoa/notation.ma ground_2/xoa/xoa.ma
-
XOA_DIR := ../../../components/binaries/xoa
XOA := xoa.native
+XOA_CONF := ground/xoa.conf.xml
XOA_OPTS := ../../matita.conf.xml $(XOA_CONF)
-XOA2_CONF := ground_2/xoa2.conf.xml
-XOA2_OPTS := ../../matita.conf.xml $(XOA2_CONF)
-
DEP_INPUT := .depend
DEP_DIR := ../../../components/binaries/matitadep
DEP := matitadep.native
PRB := probe.native
PRB_OPTS := $(XOA_OPTS) -g -i
-ORIG := . ./orig.sh
+ORIG := . ./orig.sh
ORIGS := basic_2/basic_1.orig
-CONTRIB := lambdadelta_2
-
WWW := ../../../../helm/www/lambdadelta
-TAGS := all xoa xoa2 orig elim deps top leaf stats tbls odeps trim contrib clean \
- www up-html
+TAGS := all names xoa orig elim deps top leaf stats tbls odeps trim clean \
+ pack-ground pack-2a pack-2b \
+ home up-home \
-PACKAGES := ground_2 static_2 basic_2 apps_2 alpha_1
-XPACKAGES := ground_2 static_2 basic_2
+PACKAGES := ground basic_2A static_2 basic_2 apps_2 alpha_1 delayed_updating
LDWS := $(shell find -name "*.ldw.xml")
TBLS := $(shell find -name "*.tbl")
$(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG))))
-# XMAS #######################################################################
+# names ######################################################################
-define XMAS_TEMPLATE
- XMAS += $$(MAS_$(1))
-endef
+NAMES = basic_1A basic_2A static_2 basic_2
-$(foreach PKG, $(XPACKAGES), $(eval $(call XMAS_TEMPLATE,$(PKG))))
+%/names.txt: %/*/*.ma
+ @echo "PROBE $* -ns"
+ $(H)$(PRB_DIR)/$(PRB) $(PRB_OPTS) $* -ns | sort > $@
-# xoa ########################################################################
+names: $(NAMES:%=%/names.txt)
-xoa: $(XOA_TARGETS)
+# xoa ########################################################################
-$(XOA_TARGETS): $(XOA_CONF)
+xoa: $(XOA_CONF)
@echo " EXEC $(XOA) $(XOA_CONF)"
- $(H)$(XOA_DIR)/$(XOA) $(XOA_OPTS)
-
-# xoa2 #######################################################################
-
-xoa2: $(XOA2_CONF)
- @echo " EXEC $(XOA) $(XOA2_CONF)"
- $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) -s $(XOA2_OPTS)
+ $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) -s $(XOA_OPTS)
# elim #######################################################################
$(DEP_INPUT): $(MAS) Makefile
@echo " GREP include"
$(H)grep "include \"" $(MAS) > $(DEP_INPUT)
- $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' >> $(DEP_INPUT)
+ $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' >> $(DEP_INPUT)
# dep ########################################################################
$$(STT_$(1)): P4 = $$(shell grep "qed[.-]" $$(MAS_$(1)) | wc -l)
$$(STT_$(1)): D1 = $$(word 5, $$(C0))
$$(STT_$(1)): D2 = $$(word 7, $$(C0))
- $$(STT_$(1)): D3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l)
+ $$(STT_$(1)): D3 = $$(shell grep "defined[.-]" $$(MAS_$(1)) | wc -l)
$$(STT_$(1)): M1 = $$(word 6, $$(C0))
$$(STT_$(1)): M2 = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l)
$$(STT_$(1)): M3 = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l)
@printf '%-15s %-46s' 'Statistics for:' $(1)
@printf '\x1B[0m\n'
@printf '\x1B[1;40;35m'
- @printf '%-12s' ''
+ @printf '%-12s' ''
@printf ' %-8s %6i' Chars $$(C2)
@printf ' %-7s %7i' Nodes $$(C3)
@printf ' %-11s' ''
$$(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)): S5 = $$(shell printf "%.1f" `echo "scale=2;if($$(S2)!=0)$$(S4)/$$(S2) else 0"|bc`)
$$(SUM_$(1)): C1 = $$(word 5, $$(C0))
$$(SUM_$(1)): C2 = $$(word 7, $$(C0))
$$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc)
trim: $(TRIMS:%=%.trimmed)
-# contrib ####################################################################
+# package ground #############################################################
+
+pack-ground: PKG = lambdadelta_ground
+
+pack-ground: DIRS = ground
+
+pack-ground: PMAS = $(shell find $(DIRS) -name *.ma)
+
+pack-ground:
+ @echo " TAR -cjf $(PKG).tar.bz2 root $(DIRS)"
+ $(H)tar -cjf $(PKG).tar.bz2 ../lambdadelta/root $(PMAS:%=../lambdadelta/%)
+
+# package 2A ###################################################################
+
+pack-2a: PKG = lambdadelta_2A
+
+pack-2a: DIRS = basic_2A
+
+pack-2a: PMAS = $(shell find $(DIRS) -name *.ma)
+
+pack-2a:
+ @echo " TAR -cjf $(PKG).tar.bz2 $(DIRS)"
+ $(H)tar -cjf $(PKG).tar.bz2 $(PMAS:%=../lambdadelta/%)
+
+# package 2B ###################################################################
+
+pack-2b: PKG = lambdadelta_2B
+
+pack-2b: DIRS = static_2 basic_2
+
+pack-2b: PMAS = $(shell find $(DIRS) -name *.ma)
-contrib:
- @echo " TAR -czf $(CONTRIB).tar.gz root $(XPACKAGES)"
- $(H)tar -czf $(CONTRIB).tar.gz root $(XMAS)
+pack-2b:
+ @echo " TAR -cjf $(PKG).tar.bz2 $(DIRS)"
+ $(H)tar -cjf $(PKG).tar.bz2 $(PMAS:%=../lambdadelta/%)
# 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
##############################################################################