Topic: lean4-mode C-c C-n?
Jason Gross (Mar 11 2021 at 20:04):
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 (Mar 11 2021 at 20:25):
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 (Mar 11 2021 at 20:37):
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 (Mar 11 2021 at 21:46):
Interesting, I haven't really touched the import system (on either side) in quite a while
Jason Gross (Mar 11 2021 at 21:59):
Error processing message (wrong-type-argument hash-table-p nil).
Sebastian Ullrich (Mar 11 2021 at 22:11):
I haven't seen that before. Could you get me a stacktrace using
Sebastian Ullrich (Mar 11 2021 at 22:12):
lean executable from the same commit mentioned above?
Last updated: May 18 2021 at 23:14 UTC