lean4-mode C-c C-n?

Stream: lean4

[Jason Gross]

https://github.com/leanprover/lean4/tree/master/lean4-mode#key-bindings-and-commands mentions C-c C-n for lean-toggle-next-error, but it does not seem to work anymore since I pulled 03bd608b00 (it seemed to work when I was using 152a84c468)

[Sebastian Ullrich]

Thanks for reporting, I merged it with the goal view into a new "info view" (C-c C-i) inspired by vscode-lean but did not update the README. Do tell me what you think of it. There are not many Lean 4 users, and even fewer of them using Emacs.

[Jason Gross]

Thanks! I'll try it soon, but for now I've reverted back to the older version of lean4-mode, which does not seem to suffer from the instability I've asked about at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lean4-mode.20emacs.20issues/near/229914818

[Sebastian Ullrich]

Interesting, I haven't really touched the import system (on either side) in quite a while

[Jason Gross]

I get

Error processing message (wrong-type-argument hash-table-p nil).

[Sebastian Ullrich]

I haven't seen that before. Could you get me a stacktrace using M-x toggle-debug-on-error?

[Sebastian Ullrich]

Is you lean executable from the same commit mentioned above?