From a916c8ef60843bf14f92c0af3b01e77b5c466f44 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi 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