aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-16 16:52:04 +0000
committerGitHub2020-11-16 16:52:04 +0000
commit29dc0d5b8951bb467bb2cc473a90e8feaadbb9b8 (patch)
treed810f14bebd5da3d0c8e2612e4d0da317c9cb0cd /toplevel
parentaf96434d2991b9f01f6cd3963ed114b57e40792f (diff)
parent6a6069d55f0be157ff177150594fabcbc4b1f283 (diff)
Merge PR #13040: [gc] Set GC policy as best-fit in OCaml >= 4.10.0
Reviewed-by: gares Reviewed-by: ppedrot
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml17
1 files changed, 14 insertions, 3 deletions
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: