Stack overflow during extraction

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2824
From: @Ptival
Reported version: 8.5

[coqbot]

Comment author: @Ptival

Created attachment 347
Patching mktable to use Hashtbl.replace

Gabriel Scherer and I investigated a bug where, at some point, Recursive Extraction Library would fail due to a Stack_overflow.

---

The stack overflow happens in ocaml's stdlib/hashtbl.ml, when an add operation results in a call to resize, and one particular bucket has a huge collision list.

Manually tracing the source of the problem back in Coq code leads to plugins/extraction/ocaml.ml, somewhere in pp_module_type in the case MTsig.

---

The proposed fix patches the mktable function in plugins/extraction/common.ml, so that it uses Hashtbl.replace instead of Hashtbl.add.

We believe this is safe since the hash table is closed over, and mktable only exposes its add, find and clear related functions. The semantics of replace should therefore match the one of add.

This should benefit at least in space. Time may be impacted in a positive or negative way, since replace has more work to find bindings when collisions occur, but does not need to call resize on existing keys.

---

As a side note, it seems unfortunate that Coq handles stack overflows in toplevel/cerrors.ml, and hides away the backtrace. I tried to circumvent this, but anyway my backtrace was already messed up somehow, I did not investigate this further.

---

Patch attached.
Should work both on 8.3 and 8.4.

Attached file: add_replace.patch (text/plain, 541 bytes)
Description: Patching mktable to use Hashtbl.replace

[coqbot]

Comment author: @letouzey

Hi

Thanks for the suggestion. Patch applied in branches 8.3, 8.4 and trunk.

Pierre Letouzey