Stream: Coq devs & plugin devs

Topic: change gc during require?


view this post on Zulip Gaëtan Gilbert (Nov 20 2020 at 18:57):

would adding a wrapper like

let rec_intern_library ~lib_resolver libs x =
  let gc = Gc.get () in
  try
    Gc.set {gc with Gc.minor_heap_size = 1024 * 1024 * 1024;};
    let v = rec_intern_library ~lib_resolver libs x in
    Gc.set gc;
    v
  with e ->
    Gc.set gc;
    raise e

improve timings?

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 19:00):

IIRC OCaml unmarshalling allocates the memory in one go, so probably no.

view this post on Zulip Pierre-Marie Pédrot (Nov 20 2020 at 19:06):

I confirm that the memory is allocated at once (see intern_alloc in intern.c)

view this post on Zulip Guillaume Melquiond (Nov 20 2020 at 21:05):

Notwithstanding the matter of marshalling, note that, if the GC cannot allocate the requested minor heap, then Coq will just die. Here, with such a high setting, OCaml will try to allocate the largest possible minor heap, which should be something like 1GB on a 32-bit system and 2GB on a 64-bit system. I am not sure a 32-bit Coq can survive long with such a large contiguous block of memory.


Last updated: Oct 16 2021 at 02:03 UTC