diff options
| author | coqbot-app[bot] | 2020-11-16 16:52:04 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 16:52:04 +0000 |
| commit | 29dc0d5b8951bb467bb2cc473a90e8feaadbb9b8 (patch) | |
| tree | d810f14bebd5da3d0c8e2612e4d0da317c9cb0cd /toplevel | |
| parent | af96434d2991b9f01f6cd3963ed114b57e40792f (diff) | |
| parent | 6a6069d55f0be157ff177150594fabcbc4b1f283 (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.ml | 17 |
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: |
