Coq is a heavy user of persistent data structures and symbolic ASTs, so the

minor heap is heavily sollicited. Unfortunately, the default size is far too
small, so we enlarge it a lot (128 times larger).

To better handle huge memory consumers, we also augment the default major
heap increment and the GC pressure coefficient.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15953 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index fd7dfe89b..dc131a1a5 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -135,6 +135,25 @@ let set_vm_opt () =
   Vm.set_transp_values (not !boxed_val);
   Vconv.set_use_vm !use_vm
 
+(** GC tweaking *)
+
+(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
+    minor heap is heavily sollicited. Unfortunately, the default size is far too
+    small, so we enlarge it a lot (128 times larger).
+
+    To better handle huge memory consumers, we also augment the default major
+    heap increment and the GC pressure coefficient.
+*)
+
+let init_gc () =
+  let control = Gc.get () in
+  let tweaked_control = { control with
+    Gc.minor_heap_size = 33554432; (** 4M *)
+    Gc.major_heap_increment = 268435456; (** 32M *)
+    Gc.space_overhead = 120;
+  } in
+  Gc.set tweaked_control
+
 (*s Parsing of the command line.
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
@@ -323,6 +342,7 @@ let parse_args arglist =
     | e -> fatal_error (Errors.print e)
 
 let init arglist =
+  init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   Lib.init();
   (* Default Proofb Mode starts with an alternative default. *)