Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0

Reviewed-by: gares
Reviewed-by: ppedrot

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).

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: