From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
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;