Stack Overflow

Stream: lean4

[Marcus Rossel]

I just updated to nightly-2022-06-19 and now I'm getting the following error quite frequently:

Error updating: Error fetching goals:
{
"stack":
    "Error: Server process for file:///Users/marcus/Desktop/reactor-model/src/ReactorModel/Execution/Determinism.lean crashed, likely due to a stack overflow or a bug.
        at /Users/marcus/.vscode/extensions/leanprover.lean4-0.0.78/dist/extension.js:2:542515
        at /Users/marcus/.vscode/extensions/leanprover.lean4-0.0.78/dist/extension.js:2:542809
        at Immediate.<anonymous> (/Users/marcus/.vscode/extensions/leanprover.lean4-0.0.78/dist/extension.js:2:543171)
        at processImmediate (node:internal/timers:464:21)
    ",
"message":"Server process for file:///Users/marcus/Desktop/reactor-model/src/ReactorModel/Execution/Determinism.lean crashed, likely due to a stack overflow or a bug.",
"code":-32902
}

I have no idea how to get a MWE for this, but I can offer a project that might reproduce the bug:
https://github.com/marcusrossel/reactor-model/tree/4eeea7cbebcc702a02c439bccf4efab81bbdcc34
I've marked spots that cause the crash with "CRASH" in a comment. Uncommenting the code that's in the same comment causes a crash for me.

[Wojciech Nawrocki]

Can you see if the error persists in 2022-06-20? There was a stack overflow fixed.

[Henrik Böving]

As a general remark: If I see a compiler update breaking big things in my code where I can't just find the part that broke via a gdb bt I tend to "bisect delete" my work so, keep removing stuff from the file until things work again similar to a git bisect and try to narrow it down that way, takes a bit of time but you can (in not too large projects) usually isolate an MWE.

[Edward Ayers]

Sorry for the overflows

[Chris Lovett]

Sorry is even better if it comes with new unit tests :-) Or did the unit tests catch this but we have a problem with verification during stack overflows because the process dies?

[Edward Ayers]

i missed a unit test for this case