From 6a6069d55f0be157ff177150594fabcbc4b1f283 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 16 Sep 2020 22:20:13 +0200
Subject: [gc] Set GC policy as best-fit in OCaml >= 4.10.0

Closes #11277 ; the `space_overhead` parameter has been selected for
maximum speedup, in some cases it could also increase memory
consumption. Please use `OCAMLRUNPARAM` to tune it and report back
your experiments.
---
 toplevel/coqtop.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index bbcfcc4826..d0d50aee70 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -149,6 +149,18 @@ let print_query opts = function
     heap increment and the GC pressure coefficient.
 *)
 
+let set_gc_policy () =
+  Gc.set { (Gc.get ()) with
+           Gc.minor_heap_size = 32*1024*1024 (* 32Mwords x 8 bytes/word = 256Mb *)
+         ; Gc.space_overhead = 120
+         }
+
+let set_gc_best_fit () =
+  Gc.set { (Gc.get ()) with
+           Gc.allocation_policy = 2      (* best-fit *)
+         ; Gc.space_overhead = 200
+         }
+
 let init_gc () =
   try
     (* OCAMLRUNPARAM environment variable is set.
@@ -160,9 +172,8 @@ let init_gc () =
     (* OCAMLRUNPARAM environment variable is not set.
      * In this case, we put in place our preferred configuration.
      *)
-    Gc.set { (Gc.get ()) with
-             Gc.minor_heap_size = 32*1024*1024; (* 32Mwords x 8 bytes/word = 256Mb *)
-             Gc.space_overhead = 120}
+    set_gc_policy ();
+    if Coq_config.caml_version_nums >= [4;10;0] then set_gc_best_fit () else ()
 
 let init_process () =
   (* Coq's init process, phase 1:
-- 
cgit v1.2.3