From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 11 Mar 2009 18:39:42 +0000 (+0000)
Subject: matitacLib: Gc.compact added after the compilation of mmas
X-Git-Tag: make_still_working~4154
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a916c8ef60843bf14f92c0af3b01e77b5c466f44;p=helm.git

matitacLib: Gc.compact added after the compilation of mmas
            Now LAMBDA-TYPES compiles in ~ 100m
Makefile: daily test of LAMBDA-TYPES re-enabled
---

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 6bdba1baf..28cc4c24f 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -197,7 +197,7 @@ TEST_DIRS = 				\
 #	library_auto 			
 TEST_DIRS_OPT = 			\
 	$(TEST_DIRS)                    \
-	# contribs/LAMBDA-TYPES 	\
+	contribs/LAMBDA-TYPES 		\
 	$(NULL)
 
 .PHONY: tests tests.opt cleantests cleantests.opt
diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index ff9fb1d73..cfec1c507 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -381,6 +381,10 @@ module F =
       with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None
     ;;
 
+(* FG: a problem was noticed in relising memory between subsequent *)
+(*     invocations of the compiler. The following might help       *)
+    let compact r = Gc.compact (); r
+
     let build options fname =
       let matita_debug = Helm_registry.get_bool "matita.debug" in
       let compile opts fname =
@@ -404,10 +408,10 @@ module F =
          let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
          let atexit = dump generated in
          let res = compile options fname in
-         let r = atexit res in
+         let r = compact (atexit res) in
          if r then r else begin
-           Sys.remove generated;
-           Printf.printf "rm %s\n" generated; flush stdout; r
+            Sys.remove generated;
+            Printf.printf "rm %s\n" generated; flush stdout; r
          end
       else
          compile options fname