From 99c309a47affab5a6e377d10ad77a2a65fec5455 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 23 Feb 2008 21:58:11 +0000 Subject: [PATCH] LAMBDA-TYPES: we introduced incremental dependences build to speed up the compilation dependences are now dynamic so the file "depends" was removed from svn --- .../matita/contribs/LAMBDA-TYPES/Makefile | 49 ++-- .../matita/contribs/LAMBDA-TYPES/depends | 244 ------------------ helm/software/matita/matitadep.ml | 14 +- 3 files changed, 37 insertions(+), 270 deletions(-) delete mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/depends diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index a2a3b8eec..569dd292b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -6,31 +6,35 @@ DIR=$(shell basename $$PWD) MMAS = $(shell find Base-2 -name "*.mma") MAS = $(MMAS:%.mma=%.ma) -XMAS = Base-2/theory.ma pippo +XMAS = Base-2/theory.ma -%.ma: %.mma - $(H)../../matitac.opt $(MATITAOPTIONS) `../../matitadep.opt -stdout $<` 2> /dev/null - $(H)../../matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null - $(H)$(MAKE) --no-print-directory depend.opt +$(DIR) all: depends + $(H)$(MAKE) --no-print-directory build -$(DIR) all: $(MAS) - $(H)$(MAKE) --no-print-directory depend.full +$(DIR).opt opt all.opt: depends + $(H)$(MAKE) --no-print-directory build.opt + +build: $(MAS) + $(H)$echo Base-2/theory.ma `../../matitadep.opt -stdout Base-2/theory.ma` >> depends $(H)../../matitac $(MATITAOPTIONS) 2> /dev/null -$(DIR).opt opt all.opt: $(MAS) - $(H)$(MAKE) --no-print-directory depend.full.opt + $(H)rm depends + +build.opt: $(MAS) + $(H)echo Base-2/theory.ma `../../matitadep.opt -stdout Base-2/theory.ma` >> depends $(H)../../matitac.opt $(MATITAOPTIONS) 2> /dev/null + $(H)rm depends + clean: $(H)../../matitaclean - $(H)rm -f $(MAS) - $(H)$(MAKE) --no-print-directory depend + $(H)rm -f $(MAS) depends + clean.opt: $(H)../../matitaclean.opt - $(H)rm -f $(MAS) - $(H)$(MAKE) --no-print-directory depend.opt + $(H)rm -f $(MAS) depends + clean.ma: $(H)../../matitaclean.opt $(MAS) - $(H)rm -f $(MAS) - $(H)$(MAKE) --no-print-directory depend.opt + $(H)rm -f $(MAS) depends depend: @echo matitadep @@ -40,13 +44,12 @@ depend.opt: @echo matitadep.opt $(H)../../matitadep.opt $(foreach FILE,$(XMAS),-exclude $(FILE)) $(H)cat Base-2/depends >> depends -depend.full: - @echo matitadep - $(H)../../matitadep - $(H)cat Base-2/depends >> depends -depend.full.opt: - @echo matitadep.opt - $(H)../../matitadep.opt - $(H)cat Base-2/depends >> depends + +depends: depend.opt + +%.ma: %.mma + $(H)../../matitac.opt $(MATITAOPTIONS) `../../matitadep.opt -stdout $<` 2> /dev/null + $(H)../../matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null + $(H)echo $@ `../../matitadep.opt -stdout $@` >> depends include Base-2/.depend diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends deleted file mode 100644 index a4314a81c..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/depends +++ /dev/null @@ -1,244 +0,0 @@ -Unified-Sub/preamble.ma NLE/nplus.ma NLE/props.ma NPlus/monoid.ma datatypes/Bool.ma logic/equality.ma -Unified-Sub/datatypes/Term.ma Unified-Sub/preamble.ma -Unified-Sub/datatypes/Context.ma Unified-Sub/datatypes/Term.ma -Unified-Sub/Lift/inv.ma Unified-Sub/Lift/defs.ma -Unified-Sub/Lift/defs.ma Unified-Sub/datatypes/Term.ma -Unified-Sub/Lift/props.ma Unified-Sub/Lift/fun.ma -Unified-Sub/Lift/fun.ma Unified-Sub/Lift/inv.ma -LambdaDelta-2/preamble.ma Base-2/preamble.ma LambdaDelta-1/definitions.ma -LambdaDelta-1/theory.ma LambdaDelta-1/ex0/props.ma LambdaDelta-1/ex1/props.ma LambdaDelta-1/ex2/props.ma LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-1/subst0/tlt.ma LambdaDelta-1/tau1/cnt.ma LambdaDelta-1/ty3/dec.ma LambdaDelta-1/ty3/nf2.ma LambdaDelta-1/ty3/tau0.ma LambdaDelta-1/wcpr0/fwd.ma -LambdaDelta-1/spare.ma LambdaDelta-1/theory.ma -LambdaDelta-1/preamble.ma Base-1/theory.ma -LambdaDelta-1/definitions.ma LambdaDelta-1/aprem/defs.ma LambdaDelta-1/cimp/defs.ma LambdaDelta-1/clen/defs.ma LambdaDelta-1/cnt/defs.ma LambdaDelta-1/csuba/defs.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/csubt/defs.ma LambdaDelta-1/ex0/defs.ma LambdaDelta-1/ex1/defs.ma LambdaDelta-1/ex2/defs.ma LambdaDelta-1/flt/defs.ma LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/iso/defs.ma LambdaDelta-1/llt/defs.ma LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/subst1/defs.ma LambdaDelta-1/tau1/defs.ma LambdaDelta-1/tlt/defs.ma LambdaDelta-1/wcpr0/defs.ma -LambdaDelta-1/ex0/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma -LambdaDelta-1/ex0/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/ex0/defs.ma LambdaDelta-1/leq/defs.ma -LambdaDelta-1/ex2/defs.ma LambdaDelta-1/C/defs.ma -LambdaDelta-1/ex2/props.ma LambdaDelta-1/arity/fwd.ma LambdaDelta-1/ex2/defs.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/fwd.ma -LambdaDelta-1/tlist/defs.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/tlist/props.ma LambdaDelta-1/tlist/defs.ma -LambdaDelta-1/csubt/defs.ma LambdaDelta-1/ty3/defs.ma -LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/csubt/defs.ma -LambdaDelta-1/csubt/props.ma LambdaDelta-1/csubt/defs.ma -LambdaDelta-1/csubt/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubt/defs.ma -LambdaDelta-1/csubt/drop.ma LambdaDelta-1/csubt/defs.ma LambdaDelta-1/drop/fwd.ma -LambdaDelta-1/csubt/getl.ma LambdaDelta-1/csubt/clear.ma LambdaDelta-1/csubt/drop.ma LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/getl/clear.ma -LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/getl.ma LambdaDelta-1/pc3/left.ma -LambdaDelta-1/csubt/ty3.ma LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/props.ma -LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/defs.ma -LambdaDelta-1/csubc/props.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma -LambdaDelta-1/csubc/csuba.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma -LambdaDelta-1/csubc/drop.ma LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/sc3/props.ma -LambdaDelta-1/csubc/drop1.ma LambdaDelta-1/csubc/drop.ma -LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/fwd.ma -LambdaDelta-1/csubc/getl.ma LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/drop.ma -LambdaDelta-1/csubc/arity.ma LambdaDelta-1/csubc/csuba.ma -LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/csubc/defs.ma -LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-1/csubst0/props.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/ty3/props.ma -LambdaDelta-1/ty3/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/pc3/defs.ma -LambdaDelta-1/ty3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/ty3/defs.ma -LambdaDelta-1/ty3/props.ma LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/ty3/fwd.ma -LambdaDelta-1/ty3/subst1.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/ty3/props.ma -LambdaDelta-1/ty3/pr3_props.ma LambdaDelta-1/ty3/pr3.ma -LambdaDelta-1/ty3/pr3.ma LambdaDelta-1/csubt/ty3.ma LambdaDelta-1/pc1/props.ma LambdaDelta-1/pc3/pc1.ma LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-1/ty3/subst1.ma -LambdaDelta-1/ty3/tau0.ma LambdaDelta-1/tau0/defs.ma LambdaDelta-1/ty3/pr3_props.ma -LambdaDelta-1/ty3/arity.ma LambdaDelta-1/arity/pr3.ma LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/ty3/pr3_props.ma -LambdaDelta-1/ty3/dec.ma LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/flt.ma LambdaDelta-1/pc3/dec.ma -LambdaDelta-1/ty3/arity_props.ma LambdaDelta-1/sc3/arity.ma LambdaDelta-1/ty3/arity.ma -LambdaDelta-1/ty3/nf2.ma LambdaDelta-1/nf2/arity.ma LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/ty3/arity.ma -LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/defs.ma -LambdaDelta-1/pc3/props.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr3.ma -LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/pc3/left.ma -LambdaDelta-1/pc3/pc1.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr1.ma -LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/wcpr0/getl.ma -LambdaDelta-1/pc3/left.ma LambdaDelta-1/pc3/props.ma -LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/fwd.ma -LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pc3/defs.ma -LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/subst1.ma -LambdaDelta-1/pc3/dec.ma LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/ty3/arity_props.ma -LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/defs.ma -LambdaDelta-1/pc1/props.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/pr1.ma -LambdaDelta-1/ex1/defs.ma LambdaDelta-1/C/defs.ma -LambdaDelta-1/ex1/props.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/ex1/defs.ma LambdaDelta-1/leq/props.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/nf2/props.ma LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/ty3/fwd.ma -LambdaDelta-1/sc3/defs.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/sn3/defs.ma -LambdaDelta-1/sc3/props.ma LambdaDelta-1/arity/aprem.ma LambdaDelta-1/arity/lift1.ma LambdaDelta-1/csuba/arity.ma LambdaDelta-1/drop1/getl.ma LambdaDelta-1/drop1/props.ma LambdaDelta-1/lift1/props.ma LambdaDelta-1/llt/props.ma LambdaDelta-1/nf2/lift1.ma LambdaDelta-1/sc3/defs.ma LambdaDelta-1/sn3/lift1.ma -LambdaDelta-1/sc3/arity.ma LambdaDelta-1/csubc/arity.ma LambdaDelta-1/csubc/drop1.ma LambdaDelta-1/csubc/getl.ma LambdaDelta-1/csubc/props.ma -LambdaDelta-1/sn3/defs.ma LambdaDelta-1/pr3/defs.ma -LambdaDelta-1/sn3/nf2.ma LambdaDelta-1/nf2/dec.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/sn3/defs.ma -LambdaDelta-1/sn3/props.ma LambdaDelta-1/nf2/iso.ma LambdaDelta-1/pr3/iso.ma LambdaDelta-1/sn3/fwd.ma LambdaDelta-1/sn3/nf2.ma -LambdaDelta-1/sn3/lift1.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/sn3/props.ma -LambdaDelta-1/sn3/fwd.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/sn3/defs.ma -LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/defs.ma -LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/T/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/clen.ma LambdaDelta-1/subst0/dec.ma -LambdaDelta-1/nf2/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/fwd.ma -LambdaDelta-1/nf2/arity.ma LambdaDelta-1/arity/subst0.ma LambdaDelta-1/nf2/fwd.ma -LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr3/pr3.ma -LambdaDelta-1/nf2/lift1.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/nf2/props.ma -LambdaDelta-1/nf2/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pr3/fwd.ma -LambdaDelta-1/nf2/dec.ma LambdaDelta-1/C/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr0/dec.ma LambdaDelta-1/pr2/clen.ma LambdaDelta-1/pr2/fwd.ma -LambdaDelta-1/csuba/defs.ma LambdaDelta-1/arity/defs.ma -LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/csuba/defs.ma -LambdaDelta-1/csuba/props.ma LambdaDelta-1/csuba/defs.ma -LambdaDelta-1/csuba/arity.ma LambdaDelta-1/T/props.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/csuba/getl.ma LambdaDelta-1/csuba/props.ma -LambdaDelta-1/csuba/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csuba/defs.ma -LambdaDelta-1/csuba/drop.ma LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/drop/fwd.ma -LambdaDelta-1/csuba/getl.ma LambdaDelta-1/csuba/clear.ma LambdaDelta-1/csuba/drop.ma LambdaDelta-1/getl/clear.ma -LambdaDelta-1/wcpr0/getl.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/wcpr0/defs.ma -LambdaDelta-1/wcpr0/fwd.ma LambdaDelta-1/wcpr0/defs.ma -LambdaDelta-1/wcpr0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/pr0/defs.ma -LambdaDelta-1/pr3/defs.ma LambdaDelta-1/pr2/defs.ma -LambdaDelta-1/pr3/subst1.ma LambdaDelta-1/pr2/subst1.ma LambdaDelta-1/pr3/defs.ma -LambdaDelta-1/pr3/props.ma LambdaDelta-1/pr1/props.ma LambdaDelta-1/pr2/props.ma LambdaDelta-1/pr3/pr1.ma -LambdaDelta-1/pr3/pr1.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr3/defs.ma -LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/wcpr0/getl.ma -LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/pr2/fwd.ma LambdaDelta-1/pr3/props.ma -LambdaDelta-1/pr3/pr3.ma LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/pr3/props.ma -LambdaDelta-1/pr3/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/tlist/props.ma -LambdaDelta-1/pr2/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/pr0/defs.ma -LambdaDelta-1/pr2/props.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/props.ma LambdaDelta-1/pr2/defs.ma -LambdaDelta-1/pr2/fwd.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr2/defs.ma -LambdaDelta-1/pr2/subst1.ma LambdaDelta-1/csubst1/fwd.ma LambdaDelta-1/csubst1/getl.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr2/defs.ma LambdaDelta-1/subst1/subst1.ma -LambdaDelta-1/pr2/clen.ma LambdaDelta-1/clen/getl.ma LambdaDelta-1/pr2/props.ma -LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr2/defs.ma -LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr0/defs.ma -LambdaDelta-1/pr1/props.ma LambdaDelta-1/T/props.ma LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/subst1/props.ma -LambdaDelta-1/pr1/pr1.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr1/props.ma -LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr0/props.ma LambdaDelta-1/subst1/defs.ma -LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/defs.ma -LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr0/props.ma -LambdaDelta-1/pr0/props.ma LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/subst0.ma -LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/pr0/fwd.ma -LambdaDelta-1/pr0/dec.ma LambdaDelta-1/T/dec.ma LambdaDelta-1/T/props.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/subst0/dec.ma -LambdaDelta-1/tau1/defs.ma LambdaDelta-1/tau0/defs.ma -LambdaDelta-1/tau1/props.ma LambdaDelta-1/tau0/props.ma LambdaDelta-1/tau1/defs.ma -LambdaDelta-1/tau1/cnt.ma LambdaDelta-1/cnt/props.ma LambdaDelta-1/tau1/props.ma -LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/leq/defs.ma -LambdaDelta-1/arity/fwd.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/leq/asucc.ma LambdaDelta-1/leq/fwd.ma -LambdaDelta-1/arity/subst0.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst0/props.ma LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/subst0/dec.ma LambdaDelta-1/subst0/fwd.ma -LambdaDelta-1/arity/props.ma LambdaDelta-1/arity/fwd.ma -LambdaDelta-1/arity/pr3.ma LambdaDelta-1/arity/subst0.ma LambdaDelta-1/csuba/arity.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr3/defs.ma LambdaDelta-1/wcpr0/getl.ma -LambdaDelta-1/arity/lift1.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/drop1/defs.ma -LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/cimp/props.ma -LambdaDelta-1/arity/aprem.ma LambdaDelta-1/aprem/props.ma LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/props.ma -LambdaDelta-1/aprem/defs.ma LambdaDelta-1/A/defs.ma -LambdaDelta-1/aprem/props.ma LambdaDelta-1/aprem/defs.ma LambdaDelta-1/leq/defs.ma -LambdaDelta-1/llt/defs.ma LambdaDelta-1/A/defs.ma -LambdaDelta-1/llt/props.ma LambdaDelta-1/leq/defs.ma LambdaDelta-1/llt/defs.ma -LambdaDelta-1/leq/defs.ma LambdaDelta-1/aplus/defs.ma -LambdaDelta-1/leq/asucc.ma LambdaDelta-1/leq/props.ma -LambdaDelta-1/leq/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/leq/defs.ma -LambdaDelta-1/leq/fwd.ma LambdaDelta-1/leq/defs.ma -LambdaDelta-1/aplus/defs.ma LambdaDelta-1/asucc/defs.ma -LambdaDelta-1/aplus/props.ma LambdaDelta-1/aplus/defs.ma LambdaDelta-1/next_plus/props.ma -LambdaDelta-1/asucc/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma -LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/asucc/defs.ma -LambdaDelta-1/A/defs.ma LambdaDelta-1/preamble.ma -LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/csubst0/defs.ma -LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-1/fsubst0/defs.ma -LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/csubst0/defs.ma -LambdaDelta-1/csubst1/props.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/defs.ma -LambdaDelta-1/csubst1/fwd.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/props.ma -LambdaDelta-1/csubst1/getl.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst0/props.ma LambdaDelta-1/csubst1/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/subst1/props.ma -LambdaDelta-1/csubst0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/subst0/defs.ma -LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/defs.ma -LambdaDelta-1/csubst0/props.ma LambdaDelta-1/csubst0/defs.ma -LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/s/props.ma -LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubst0/fwd.ma -LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/getl/fwd.ma -LambdaDelta-1/subst0/defs.ma LambdaDelta-1/lift/defs.ma -LambdaDelta-1/subst0/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma -LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst0/props.ma -LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst0/fwd.ma -LambdaDelta-1/subst0/tlt.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/subst0/defs.ma -LambdaDelta-1/subst0/dec.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma -LambdaDelta-1/tau0/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/getl/defs.ma -LambdaDelta-1/tau0/props.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/tau0/defs.ma -LambdaDelta-1/subst1/subst1.ma LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst1/fwd.ma -LambdaDelta-1/subst1/defs.ma LambdaDelta-1/subst0/defs.ma -LambdaDelta-1/subst1/fwd.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma -LambdaDelta-1/subst1/props.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma -LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/defs.ma -LambdaDelta-1/cimp/props.ma LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/getl.ma -LambdaDelta-1/getl/defs.ma LambdaDelta-1/clear/defs.ma LambdaDelta-1/drop/defs.ma -LambdaDelta-1/getl/props.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/getl/fwd.ma -LambdaDelta-1/getl/fwd.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/getl/defs.ma -LambdaDelta-1/getl/drop.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma -LambdaDelta-1/getl/clear.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma -LambdaDelta-1/getl/getl.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma -LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/props.ma -LambdaDelta-1/getl/flt.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/flt/props.ma LambdaDelta-1/getl/fwd.ma -LambdaDelta-1/clear/defs.ma LambdaDelta-1/C/defs.ma -LambdaDelta-1/clear/fwd.ma LambdaDelta-1/clear/defs.ma -LambdaDelta-1/clear/props.ma LambdaDelta-1/clear/fwd.ma -LambdaDelta-1/clear/drop.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma -LambdaDelta-1/drop1/defs.ma LambdaDelta-1/drop/defs.ma LambdaDelta-1/lift1/defs.ma -LambdaDelta-1/drop1/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/getl/defs.ma -LambdaDelta-1/drop1/getl.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/getl/drop.ma -LambdaDelta-1/drop/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/lift/defs.ma LambdaDelta-1/r/defs.ma -LambdaDelta-1/drop/fwd.ma LambdaDelta-1/drop/defs.ma -LambdaDelta-1/drop/props.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/r/props.ma -LambdaDelta-1/lift1/defs.ma LambdaDelta-1/lift/defs.ma -LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift1/defs.ma -LambdaDelta-1/lift1/props.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/lift/props.ma -LambdaDelta-1/cnt/defs.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/cnt/props.ma LambdaDelta-1/cnt/defs.ma LambdaDelta-1/lift/fwd.ma -LambdaDelta-1/lift/defs.ma LambdaDelta-1/s/defs.ma LambdaDelta-1/tlist/defs.ma -LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift/defs.ma -LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/s/props.ma -LambdaDelta-1/lift/tlt.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/tlt/props.ma -LambdaDelta-1/iso/props.ma LambdaDelta-1/iso/fwd.ma -LambdaDelta-1/iso/fwd.ma LambdaDelta-1/iso/defs.ma LambdaDelta-1/tlist/defs.ma -LambdaDelta-1/iso/defs.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/G/defs.ma LambdaDelta-1/preamble.ma -LambdaDelta-1/flt/props.ma LambdaDelta-1/C/props.ma LambdaDelta-1/flt/defs.ma -LambdaDelta-1/flt/defs.ma LambdaDelta-1/C/defs.ma -LambdaDelta-1/tlt/props.ma LambdaDelta-1/tlt/defs.ma -LambdaDelta-1/tlt/defs.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/T/props.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/T/dec.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/T/defs.ma LambdaDelta-1/preamble.ma -LambdaDelta-1/s/props.ma LambdaDelta-1/s/defs.ma -LambdaDelta-1/s/defs.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/C/props.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/T/props.ma -LambdaDelta-1/C/defs.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/r/props.ma LambdaDelta-1/r/defs.ma LambdaDelta-1/s/defs.ma -LambdaDelta-1/r/defs.ma LambdaDelta-1/T/defs.ma -LambdaDelta-1/next_plus/props.ma LambdaDelta-1/next_plus/defs.ma -LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/G/defs.ma -LambdaDelta-1/clen/getl.ma LambdaDelta-1/clen/defs.ma LambdaDelta-1/getl/props.ma -LambdaDelta-1/clen/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/s/defs.ma -Base-1/theory.ma Base-1/blt/props.ma Base-1/ext/arith.ma Base-1/ext/tactics.ma Base-1/plist/props.ma Base-1/types/props.ma -Base-1/definitions.ma Base-1/blt/defs.ma Base-1/plist/defs.ma Base-1/types/defs.ma -Base-1/preamble.ma coq.ma -Base-1/spare.ma Base-1/theory.ma -Base-1/plist/defs.ma Base-1/preamble.ma -Base-1/plist/props.ma Base-1/plist/defs.ma -Base-1/types/props.ma Base-1/types/defs.ma -Base-1/types/defs.ma Base-1/preamble.ma -Base-1/blt/props.ma Base-1/blt/defs.ma -Base-1/blt/defs.ma Base-1/preamble.ma -Base-1/ext/tactics.ma Base-1/preamble.ma -Base-1/ext/arith.ma Base-1/preamble.ma -Base-2/preamble.ma Base-1/definitions.ma -Base-2/theory.ma Base-2/blt/props.ma Base-2/ext/arith.ma Base-2/ext/tactics.ma Base-2/plist/props.ma Base-2/types/props.ma -Base-2/types/defs.ma Base-2/preamble.ma -Base-2/types/props.ma Base-2/types/defs.ma -Base-2/plist/defs.ma Base-2/preamble.ma -Base-2/plist/props.ma Base-2/plist/defs.ma -Base-2/ext/arith.ma Base-2/preamble.ma -Base-2/ext/tactics.ma Base-2/preamble.ma -Base-2/blt/defs.ma Base-2/preamble.ma -Base-2/blt/props.ma Base-2/blt/defs.ma -NLE/nplus.ma -NLE/props.ma -NPlus/monoid.ma -coq.ma -datatypes/Bool.ma -logic/equality.ma -Base-2/ext/tactics.mma Base-2/preamble.ma Base-1/ext/tactics.ma -Base-2/ext/arith.mma Base-2/preamble.ma Base-1/ext/arith.ma -Base-2/types/defs.mma Base-2/preamble.ma Base-1/types/defs.ma -Base-2/types/props.mma Base-2/preamble.ma Base-1/types/props.ma -Base-2/blt/defs.mma Base-2/preamble.ma Base-1/blt/defs.ma -Base-2/blt/props.mma Base-2/preamble.ma Base-1/blt/props.ma -Base-2/plist/defs.mma Base-2/preamble.ma Base-1/plist/defs.ma -Base-2/plist/props.mma Base-2/preamble.ma Base-1/plist/props.ma diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml index fc50a74fb..d50707f29 100644 --- a/helm/software/matita/matitadep.ml +++ b/helm/software/matita/matitadep.ml @@ -25,12 +25,15 @@ (* $Id$ *) -open Printf - module GA = GrafiteAst module U = UriManager module HR = Helm_registry +let print_times msg = + let times = Unix.times () in + let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in + Printf.printf "TIME STAMP: %s: %f\n" msg stamp; flush stdout; stamp + let fix_name f = let f = if Pcre.pmatch ~pat:"^\\./" f then String.sub f 2 (String.length f - 2) @@ -43,6 +46,7 @@ let exclude excluded_files files = List.filter map files let main () = +(* let _ = print_times "inizio" in *) let include_paths = ref [] in let excluded_files = ref [] in let use_stdout = ref false in @@ -122,7 +126,9 @@ let main () = Hashtbl.add include_deps ma_file ma_file Hashtbl.add include_deps_dot ma_file baseuri *) +(* let _ = print_times "prima di iter1" in *) List.iter (fun ma_file -> ignore (baseuri_of_script ma_file)) ma_files; +(* let _ = print_times "in mezzo alle due iter" in *) List.iter (fun ma_file -> let ma_baseuri = baseuri_of_script ma_file in @@ -145,6 +151,7 @@ let main () = dependencies) ma_files; (* generate regular depend output *) +(* let _ = print_times "dopo di iter2" in *) let deps = List.fold_left (fun acc ma_file -> @@ -188,5 +195,6 @@ let main () = ignore(Sys.command ("tred "^ !dot_file^"| dot -Tpng -o"^dot_name^".png")); HLog.message ("Type 'eog "^dot_name^".png' to view the graph"); end; -;; +(* let _ = print_times "fine" in () *) + -- 2.39.2