From: Ferruccio Guidi Date: Wed, 25 Jul 2007 14:39:14 +0000 (+0000) Subject: matitac: We do not generate the .moo and .lexicon of a dumped .mma X-Git-Tag: 0.4.95@7852~278 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ffe3843a38d4d40f9426381bf379f4be524cada0;p=helm.git matitac: We do not generate the .moo and .lexicon of a dumped .mma Base-2 : makefile patched --- diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/Makefile b/matita/contribs/LAMBDA-TYPES/Base-2/Makefile deleted file mode 100644 index 2524510f3..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/Makefile +++ /dev/null @@ -1,27 +0,0 @@ -include ../../../../Makefile.defs - -H=@ - -MATITAC = $(RT_BASE_DIR)/matitac.opt - -MMAS = $(shell find -name "*.mma") -MAS = $(MMAS:%.mma=%.ma) - -all: OPTIONS = -bench - -log: OPTIONS = >> tmp.txt 2>&1 - -all: $(MAS) - -log: $(MAS) - $(H)mv tmp.txt log.txt - -clean: - $(H)rm -f $(MAS) - -%.ma: %.mma - $(H)$(MATITAC) -dump $@ $< $(OPTIONS) - -include depend - -.DELETE_ON_ERROR: diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/depend b/matita/contribs/LAMBDA-TYPES/Base-2/depend index 1f10a0079..08a5752f9 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/depend +++ b/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 +theory.ma: theory.mma ext/tactics.ma ext/arith.ma types/props.ma blt/props.ma plist/props.ma ext/tactics.mo.opt ext/arith.mo.opt types/props.mo.opt blt/props.mo.opt plist/props.mo.opt +ext/tactics.ma: ext/tactics.mma preamble.ma preamble.mo.opt +ext/arith.ma: ext/arith.mma preamble.ma preamble.mo.opt +types/defs.ma: types/defs.mma preamble.ma preamble.mo.opt +types/props.ma: types/props.mma types/defs.ma types/defs.mo.opt +blt/defs.ma: blt/defs.mma preamble.ma preamble.mo.opt +blt/props.ma: blt/props.mma blt/defs.ma blt/defs.mo.opt +plist/defs.ma: plist/defs.mma preamble.ma preamble.mo.opt +plist/props.ma: plist/props.mma plist/defs.ma plist/defs.mo.opt diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/makefile b/matita/contribs/LAMBDA-TYPES/Base-2/makefile index 7615bb7e5..9749db39c 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/makefile +++ b/matita/contribs/LAMBDA-TYPES/Base-2/makefile @@ -1,6 +1,6 @@ H=@ -RT_BASEDIR=/home/fguidi/svn/software/matita/ +RT_BASEDIR=../../../ OPTIONS=-bench MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) @@ -27,6 +27,11 @@ clean.opt: clean_mas preall.opt cleanall.opt: clean_mas preall.opt $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all +mas: preall + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) +mas.opt: preall.opt + $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) + %.mo: preall $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ %.mo.opt: preall.opt @@ -38,14 +43,22 @@ preall: preall.opt: $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) - # FG: added part ############################################################ -build_mas: - $(H)$(MAKE) preamble.mo.opt - $(H)$(MAKE) -f Makefile - $(H)$(MAKE) preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) +MATITAC = $(RT_BASEDIR)/matitac.opt + +MMAS = $(shell find -name "*.mma") +MAS = $(MMAS:%.mma=%.ma) + +build_mas: preall.opt theory.ma clean_mas: - $(H)$(MAKE) -f Makefile clean + $(H)rm -f $(MAS) + +%.ma: %.mma + $(H)$(MATITAC) -dump $@ $< $(OPTIONS) + $(MAKE) preall.opt + +include depend + +.DELETE_ON_ERROR: diff --git a/matita/matitac.ml b/matita/matitac.ml index 31b304333..179a0ba8e 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -61,6 +61,7 @@ let pp_ast_statement st = (**) let dump f = + Helm_registry.set_bool "matita.moo" false; let floc = H.dummy_floc in let nl_ast = G.Comment (floc, G.Note (floc, "")) in let och = open_out f in @@ -87,6 +88,7 @@ let dump f = at_exit atexit let main () = + Helm_registry.set_bool "matita.moo" true; match Filename.basename Sys.argv.(0) with |"gragrep" |"gragrep.opt" |"gragrep.opt.static" ->Gragrep.main() |"matitadep" |"matitadep.opt" |"matitadep.opt.static" ->Matitadep.main() diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 8bb0dab4c..c2cdd7ef5 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -371,8 +371,11 @@ let main ~mode = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in - GrafiteMarshal.save_moo moo_fname moo_content_rev; - LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; +(* FG: we do not generate .moo when dumping .mma files *) + if Helm_registry.get_bool "matita.moo" then begin + GrafiteMarshal.save_moo moo_fname moo_content_rev; + LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; + end; HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname bench_mode true big_bang;