Stack overflow (solvable by increasing stack size)

[Blaisorblade]

Probably a low-priority issue — I'm logging it anyway in case it helps.

While installing the latest Coq platform on Apple Silicon (coq-platform.2022.04.08.152022.0, using coq-hott.8.15), I got a stack overflow/segfault:

COQC theories/Categories/Category/Sigma/Univalent.v
File "./theories/Categories/Category/Sigma/Univalent.v", line 296, characters 4-1586:
Error: Stack overflow.

COQC theories/Categories/Category/Sigma/Univalent.v
Command terminated by signal 11

The fix is to increase the soft ulimit for the stack size — ulimit -s -S 24528 will work (the default here is 8176, and ulimit -S -s $[8176*207/100] still fails; whileulimit -S -s $[8176*208/100] works).

[Blaisorblade]

A better fix is to jump to OCaml 4.14.0 instead of 4.13.1 — there 90 kilobytes are enough:

$ rm -f theories/Categories/Category/Sigma/Univalent.vo ; \
(ulimit -S -s 96 && make theories/Categories/Category/Sigma/Univalent.vo -sj10)
COQC theories/Categories/Category/Sigma/Univalent.v
theories/Categories/Category/Sigma/Univalent.vo (real: 1.15, user: 1.09, sys: 0.05, mem: 340688 ko)

[Blaisorblade]

Just for completeness, here's the lldb backtrace on OCaml 4.13.1+flambda:

(lldb) bt 200
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=2, address=0x16f603fd8)
  * frame #0: 0x0000000100c91990 coqc`caml_make_vect(len=7, init=5513782752) at array.c:212:3 [opt]
    frame #1: 0x0000000100ca9ac8 coqc`caml_c_call + 28
    frame #2: 0x0000000100c0c6f0 coqc`camlStdlib__Array__of_list_581 + 72
    frame #3: 0x000000010069cfcc coqc`camlRetyping__expand_projection_1827 + 316
    frame #4: 0x00000001006d30b0 coqc`camlConstr_matching__next_13284 + 3152
    frame #5: 0x00000001006cc124 coqc`camlConstr_matching__code_begin + 76
    frame #6: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #7: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #8: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #9: 0x00000001006cc124 coqc`camlConstr_matching__code_begin + 76
    frame #10: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #11: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #12: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #13: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #14: 0x00000001006cc124 coqc`camlConstr_matching__code_begin + 76
    frame #15: 0x00000001006d3d48 coqc`camlConstr_matching__next_3681 + 104
    frame #16: 0x00000001006cc124 coqc`camlConstr_matching__code_begin + 76
    frame #17: 0x00000001006d3a54 coqc`camlConstr_matching__try_aux_13404 + 84
    [lots more stack frames]

[k4rtik]

@Blaisorblade ran into the same issue while installing full coq-platform, perhaps this issue should also be reported at platform repo?

[Blaisorblade]

Maybe I should have; at least on Apr 18 I opened a discussion on the Coq Platform Zulip (because I wasn’t sure it was a valid issue and what to do about it) and there was some follow-up.

[Blaisorblade]

Link: https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform-devs-.26-users/topic/Coq.20Platform.20and.20stack.20overflows (I’m on my phone and in vacation, so no time to re-read it).

[Alizter]

Is there anything we can do about this in the end? It seems to be a Coq/Platform issue IIUC?