- system flag now forks for matitadep too

= legacy Base-1 and LambdaDelta-1 reinserted on tests.
  will compile in system space because they are published

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 0562ba3bbe2eb326374569c5d2dee3bdc1cdcf9d..93a6fc6cbb8a9d7d32a0f769558e76199e942151 100644 (file)
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -199,6 +199,7 @@ distclean: clean
        $(H)rm -rf .matita
 
 TEST_DIRS =                            \
+       legacy                          \
        library                         \
        tests                           \
        dama                            \

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile
index e869346aba9dca98c379f60776cf97842771e473..3198e94cfef9c7b022f1f04fbc3626f9b07a7fb1 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/makefile
@@ -1,7 +1,7 @@
-H=@
+H= @
 
 RT_BASEDIR=../../../
-OPTIONS=-bench -onepass
+OPTIONS=-bench -onepass -system
 MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
 CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
 MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile
index b8fec3cd26a4ac5df589322d24ba495e8f68564c..8f20b3276133df1d383558229170bb8a66ad0d3b 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile
@@ -1,7 +1,7 @@
 H=@
 
 RT_BASEDIR=../../../
-OPTIONS=-bench -onepass 
+OPTIONS=-bench -onepass -system
 MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
 CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
 MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index 6e29fc2daa84bc75eeb5396f115f25ad9c1cce3b..93fba67cede85250e940daded0ced5542e40b635 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -1,6 +1,6 @@
 GOALS = all opt clean clean.opt
 
-DEVELS = Base-2 Unified-Sub 
+DEVELS = Base-1 LambdaDelta-1 Base-2 Unified-Sub 
 
 $(GOALS): 
        @$(foreach DEVEL, $(DEVELS), $(MAKE) -k -C $(DEVEL) $@;) 

diff --git a/helm/software/matita/legacy/makefile b/helm/software/matita/legacy/makefile
index ec9f8cb26a5556242ec478a960943cdffefb5994..a1dd3ca335d5741c4bf0f6d567dda15104357564 100644 (file)
--- a/helm/software/matita/legacy/makefile
+++ b/helm/software/matita/legacy/makefile
@@ -1,7 +1,7 @@
 H=@
 
 RT_BASEDIR=../
-OPTIONS=-bench
+OPTIONS=-bench -onepass -system
 MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
 CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
 MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index cf821c1673b20fe5b7ab073af17df7d05c3a3778..44b09b5aea9da662033158ceea485970767ef158 100644 (file)
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -331,6 +331,8 @@ let initialize_all () =
 let parse_cmdline_and_configuration_file () =
   status := List.fold_left (fun s f -> f s) !status conf_components
 
-;;
+let initialize_environment () =
+  status := initialize_environment !status
 
-Inversion_principle.init ()
+let _ =
+  Inversion_principle.init ()

diff --git a/helm/software/matita/matitaInit.mli b/helm/software/matita/matitaInit.mli
index 272657cc3d83a8f157bda88caef4036152899165..ac0dc6a7576112cee438defbe3fff28effc29545 100644 (file)
--- a/helm/software/matita/matitaInit.mli
+++ b/helm/software/matita/matitaInit.mli
@@ -28,6 +28,7 @@ val initialize_all: unit -> unit
 
   (** {2 per-components initialization} *)
 val parse_cmdline_and_configuration_file: unit -> unit
+val initialize_environment: unit -> unit
 
   (** {2 Utilities} *)
 

diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml
index 3a5ee6561f4013628498d74cd099171843097075..cfbc3783cbae5e624e842867e038a2ee576b88e0 100644 (file)
--- a/helm/software/matita/matitadep.ml
+++ b/helm/software/matita/matitadep.ml
@@ -55,6 +55,7 @@ let main () =
     ["-dot", Arg.Set_string dot_file,
       "<file> Save dependency graph in dot format to the given file"];
   MatitaInit.parse_cmdline_and_configuration_file ();
+  MatitaInit.initialize_environment ();
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
   let args = Helm_registry.get_list Helm_registry.string "matita.args" in

diff --git a/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml
index ccfdd9bab6f937754f98fe31ed7de9e420726010..eed971f4514568a466e167165ef4781ed02c865d 100644 (file)
--- a/helm/software/matita/matitamakeLib.ml
+++ b/helm/software/matita/matitamakeLib.ml
@@ -355,7 +355,7 @@ let publish_development_bstract build clean devel =
     let orig_matita_flags = 
       try Sys.getenv "MATITA_FLAGS" with Not_found -> "" 
     in
-    "\"" ^ orig_matita_flags ^ "\"", "\"" ^ orig_matita_flags ^ " -system\"" 
+    orig_matita_flags, orig_matita_flags ^ " -system" 
   in
   HLog.message "cleaning the development before publishing";
   if clean ~matita_flags devel then

diff --git a/helm/software/matita/template_makefile.in b/helm/software/matita/template_makefile.in
index e61f757d6ee07412447adc0b3ba11aa5e8290a29..ac3e1449829f36ae6dda5c85a7f7a02487588dba 100644 (file)
--- a/helm/software/matita/template_makefile.in
+++ b/helm/software/matita/template_makefile.in
@@ -17,7 +17,7 @@ all: $(TODO)
 
 clean:
        $(MATITACLEAN) $(MATITA_FLAGS) $(SRC) 
-       rm -f $(TODO)
+       rm -f $(TODO) @DEPFILE@
 
 %.moo:
        if [ -z "$<" ]; then \