From ebb9c7470956fb56a4cad9dcd4b8491c0ed01fca Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 19 Feb 2008 19:24:14 +0000 Subject: [PATCH] dependences needed a fix :) --- .../contribs/LAMBDA-TYPES/Base-2/.depend | 18 ++++---- .../contribs/LAMBDA-TYPES/Base-2/Makefile | 30 ------------- .../contribs/LAMBDA-TYPES/Base-2/depends_mma | 18 ++++---- .../matita/contribs/LAMBDA-TYPES/Base-2/root | 1 - .../matita/contribs/LAMBDA-TYPES/Makefile | 33 ++++++++++---- .../matita/contribs/LAMBDA-TYPES/depends | 43 +++++++++++++------ .../LAMBDA-TYPES/{Base-2 => }/log.txt | 0 .../matita/contribs/LAMBDA-TYPES/root | 4 +- 8 files changed, 75 insertions(+), 72 deletions(-) delete mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile delete mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root rename helm/software/matita/contribs/LAMBDA-TYPES/{Base-2 => }/log.txt (100%) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend index 1f10a0079..800096bb8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend @@ -1,9 +1,9 @@ -theory.ma: theory.mma ext/tactics.ma ext/arith.ma types/props.ma blt/props.ma plist/props.ma -ext/tactics.ma: ext/tactics.mma preamble.ma -ext/arith.ma: ext/arith.mma preamble.ma -types/defs.ma: types/defs.mma preamble.ma -types/props.ma: types/props.mma types/defs.ma -blt/defs.ma: blt/defs.mma preamble.ma -blt/props.ma: blt/props.mma blt/defs.ma -plist/defs.ma: plist/defs.mma preamble.ma -plist/props.ma: plist/props.mma plist/defs.ma +Base-2/theory.ma: Base-2/theory.mma Base-2/ext/tactics.ma Base-2/ext/arith.ma Base-2/types/props.ma Base-2/blt/props.ma Base-2/plist/props.ma +Base-2/ext/tactics.ma: Base-2/ext/tactics.mma Base-2/preamble.ma +Base-2/ext/arith.ma: Base-2/ext/arith.mma Base-2/preamble.ma +Base-2/types/defs.ma: Base-2/types/defs.mma Base-2/preamble.ma +Base-2/types/props.ma: Base-2/types/props.mma Base-2/types/defs.ma +Base-2/blt/defs.ma: Base-2/blt/defs.mma Base-2/preamble.ma +Base-2/blt/props.ma: Base-2/blt/props.mma Base-2/blt/defs.ma +Base-2/plist/defs.ma: Base-2/plist/defs.mma Base-2/preamble.ma +Base-2/plist/props.ma: Base-2/plist/props.mma Base-2/plist/defs.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile deleted file mode 100644 index fb110c559..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/Makefile +++ /dev/null @@ -1,30 +0,0 @@ -DIR=$(shell basename $$PWD) - -MMAS = $(shell find -name "*.mma") -MAS = $(MMAS:%.mma=%.ma) - -%.ma: %.mma - ../../../matitac.opt -dump $@ $< 2>/dev/null - $(MAKE) depend.opt - ../../../matitac.opt $@ - -$(DIR) all: $(MAS) - ../../../matitac -$(DIR).opt opt all.opt: $(MAS) - ../../../matitac.opt -clean: - ../../../matitaclean - rm -f $(MAS) - $(MAKE) depend -clean.opt: - ../../../matitaclean.opt - rm -f $(MAS) - $(MAKE) depend.opt -depend: - ../../../matitadep - cat depends_mma >> depends -depend.opt: - ../../../matitadep.opt - cat depends_mma >> depends - -include .depend diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends_mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends_mma index 8bf5d1e06..7f10402a2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends_mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends_mma @@ -1,9 +1,9 @@ -theory.mma preamble.ma -ext/tactics.mma preamble.ma -ext/arith.mma preamble.ma -types/defs.mma preamble.ma -types/props.mma preamble.ma -blt/defs.mma preamble.ma -blt/props.mma preamble.ma -plist/defs.mma preamble.ma -plist/props.mma preamble.ma +Base-2/theory.mma Base-2/preamble.ma Base-1/theory.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/contribs/LAMBDA-TYPES/Base-2/root b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root deleted file mode 100644 index ef1f7b21e..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root +++ /dev/null @@ -1 +0,0 @@ -baseuri=cic:/matita/LAMBDA-TYPES/Base-2 diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index a57a7281e..17478c353 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -1,15 +1,30 @@ DIR=$(shell basename $$PWD) -MATITAOPTIONS=-onepass -$(DIR) all: - ../../../matitac $(MATITAOPTIONS) -$(DIR).opt opt all.opt: - ../../../matitac.opt $(MATITAOPTIONS) +MMAS = $(shell find -name "*.mma") +MAS = $(MMAS:%.mma=%.ma) + +%.ma: %.mma + ../../matitac.opt $< 2> /dev/null + ../../matitac.opt -dump $@ $< 2> /dev/null + $(MAKE) depend.opt + +$(DIR) all: $(MAS) + ../../matitac +$(DIR).opt opt all.opt: $(MAS) + ../../matitac.opt clean: - ../../../matitaclean + ../../matitaclean + rm -f $(MAS) + $(MAKE) depend clean.opt: - ../../../matitaclean.opt + ../../matitaclean.opt + rm -f $(MAS) + $(MAKE) depend.opt depend: - ../../../matitadep + ../../matitadep + cat Base-2/depends_mma >> depends depend.opt: - ../../../matitadep.opt + ../../matitadep.opt + cat Base-2/depends_mma >> depends + +include Base-2/.depend diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends index 9bb223d98..49056cf08 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/depends +++ b/helm/software/matita/contribs/LAMBDA-TYPES/depends @@ -1,13 +1,32 @@ -definitions.ma blt/defs.ma plist/defs.ma types/defs.ma -preamble.ma coq.ma -theory.ma blt/props.ma ext/arith.ma ext/tactics.ma plist/props.ma types/props.ma -spare.ma theory.ma -plist/props.ma plist/defs.ma -plist/defs.ma preamble.ma -ext/tactics.ma preamble.ma -ext/arith.ma preamble.ma -types/props.ma types/defs.ma -types/defs.ma preamble.ma -blt/props.ma blt/defs.ma -blt/defs.ma preamble.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 coq.ma +Base-2/theory.mma Base-2/preamble.ma Base-1/theory.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/contribs/LAMBDA-TYPES/Base-2/log.txt b/helm/software/matita/contribs/LAMBDA-TYPES/log.txt similarity index 100% rename from helm/software/matita/contribs/LAMBDA-TYPES/Base-2/log.txt rename to helm/software/matita/contribs/LAMBDA-TYPES/log.txt diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/root b/helm/software/matita/contribs/LAMBDA-TYPES/root index 43a60f943..d3e398271 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/root +++ b/helm/software/matita/contribs/LAMBDA-TYPES/root @@ -1,2 +1,2 @@ -baseuri=cic:/matita/LAMBDA-TYPES/Base-1 -include_paths= ../../../legacy +baseuri=cic:/matita/LAMBDA-TYPES +include_paths= ../../legacy -- 2.39.2