Stream: Coq devs & plugin devs

Topic: change gc during require?

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?

Pierre-Marie Pédrot (Nov 20 2020 at 19:00):

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

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)

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 08 2024 at 14:01 UTC