diff options
| author | Emilio Jesus Gallego Arias | 2020-09-16 22:20:13 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-16 15:44:42 +0100 |
| commit | 6a6069d55f0be157ff177150594fabcbc4b1f283 (patch) | |
| tree | da0609afecff04a95824697499a7f45f464b7510 /doc | |
| parent | fb186f25abeb0565bb6e238345f0c5147b697322 (diff) | |
[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.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/07-commands-and-options/13040-gc+best_fit.rst | 9 |
1 files changed, 9 insertions, 0 deletions
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). |