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 (file)
index 2524510..0000000
--- 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 1f10a0079148699bf6d6063cffd5338370ad9972..08a5752f95598d2c289859423070ba20738c4585 100644 (file)
--- 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 7615bb7e51922e822a09a3e1fb1bd763b4917676..9749db39cbfdfce123f582efc5fe2273c4c3c495 100644 (file)
--- 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 31b304333fd34e3446fe27953666273b33b5d062..179a0ba8e8e508e413f22958cef5c20cc1039fbc 100644 (file)
--- 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 8bb0dab4c2a1dd12af444535b0f10cf81e8a8376..c2cdd7ef5787e886f9629ca8bb5bb7bf27677bf4 100644 (file)
--- 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;