crash reporting

Stream: lean4

[Alex Meiburg]

sometimes in the process of pretty 'normal' use (trying to prove a theorem) I get crashes, like just now I got

PANIC at Lean.isLevelMVarAssignable Lean.MetavarContext:413:14: unknown universe metavariable

How important/useful is it for me to send these on / post them as a GitHub issue somewhere? Things always seem to keep on moving just fine (I can keep working, without even restarting the server) so it doesn't block me, so personally I feel no benefit to reporting it. But I'm curious if this is useful for the people working on the actual Lean language; if it is, I'll report more such things.

[Sebastian Ullrich]

Without a stack trace (which currently is produced on Linux only), there is no indication as to what repo it should be reported to sadly

[Alex Meiburg]

oh, I'm working on Linux, I do have the full stack trace

[Sebastian Ullrich]

Haha, that would be helpful then :big_smile:

[Alex Meiburg]

stacktrace.txt
Alright! Attached. Is here in the zulip fine, or could you point me to a GitHub to file it at?

[Sebastian Ullrich]

Interesting, that does look like a lean4 issue. If you could file that together with an MWE, that would be perfect

[Alex Meiburg]

I wasn't able to reproduce it. :') It happened kind of abruptly while typing, so I'm not even sure what code it was trying to evaluate when this happened. I'll put on GitHub best I can

[Alex Meiburg]

https://github.com/leanprover/lean4/issues/3780