...

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index a9172cee5a563b43406d37873a7eea76a72ee354..e793a725b61b3019c81ca31242729ce5c1d5d4f8 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -180,10 +180,10 @@ let activate_extraction baseuri fname =
   let f =
     open_out
      (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
-   LibrarySync.set_object_declaration_hook
-    (fun _ obj ->
+   LibrarySync.add_object_declaration_hook
+    (fun ~add_obj ~add_coercion _ obj ->
       output_string f (CicExportation.ppobj baseuri obj);
-      flush f);
+      flush f; []);
 ;;
 
 let compile options fname =
@@ -193,11 +193,11 @@ let compile options fname =
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
-  let grafite_status = GrafiteSync.init baseuri in
   let lexicon_status = 
     CicNotation2.load_notation ~include_paths:[]
       BuildTimeConf.core_notation_script 
   in
+  let grafite_status = GrafiteSync.init lexicon_status baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times () 
@@ -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