From a916c8ef60843bf14f92c0af3b01e77b5c466f44 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 11 Mar 2009 18:39:42 +0000
Subject: [PATCH] matitacLib: Gc.compact added after the compilation of mmas
Now LAMBDA-TYPES compiles in ~ 100m Makefile: daily test of
LAMBDA-TYPES re-enabled
---
helm/software/matita/Makefile | 2 +-
helm/software/matita/matitacLib.ml | 10 +++++++---
2 files changed, 8 insertions(+), 4 deletions(-)
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
--
2.39.2