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.
---
 .../07-commands-and-options/13040-gc+best_fit.rst       |  9 +++++++++
 toplevel/coqtop.ml                                      | 17 ++++++++++++++---
 2 files changed, 23 insertions(+), 3 deletions(-)
 create mode 100644 doc/changelog/07-commands-and-options/13040-gc+best_fit.rst

diff --git a/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst b/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst
new file mode 100644
index 0000000000..74818f8464
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+  When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC
+  policy, which should provide some performance benefits. Coq's policy
+  is optimized for speed, but could increase memory consumption in
+  some cases. You are welcome to tune it using the ``OCAMLRUNPARAM``
+  variable and report back setting so we could optimize more.
+  (`#13040 <https://github.com/coq/coq/pull/13040>`_,
+  fixes `#11277 <https://github.com/coq/coq/issues/11277>`_,
+  by Emilio Jesus Gallego Arias).
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