Zulip Chat Archive

Stream: lean4

Topic: lean4-mode emacs issues


view this post on Zulip Jason Gross (Mar 11 2021 at 19:55):

What should I do when lean4-mode in Emacs starts misbehaving? e.g., often when I switch files I get unknown package 'Syntax' on the first line about import, and then weird errors like expected prio at the h in high in local infix :70 (priority:=high) " ~> " => Arr, I'm told that C-c C-n is undefined when I try to view errors, etc. Restarting emacs generally fixes the issue, but I've already hit this three times in the past half-hour

view this post on Zulip Julian Berman (Mar 11 2021 at 21:00):

(I don't use emacs so ignore me if you tried it already, but probably better than trying to restart emacs immediately is restarting the language server client and seeing if that fixes it)

view this post on Zulip Jason Gross (Mar 11 2021 at 21:01):

How do I restart the language server client?

view this post on Zulip Julian Berman (Mar 11 2021 at 21:23):

Can try to figure it out in a little bit if someone who knows what they're talking about doesn't chime in, but maybe pkill -f lean will do it automaticlaly (i.e. killing the server process)

view this post on Zulip Jason Gross (Mar 11 2021 at 21:24):

Ah, I think I figured out part of the issue: when I have unsaved changes in an emacs buffer, switching to another emacs buffer tries to call leanpkg build or something, and this will fail because it will try to compile my unsaved changes in .#whatever.lean. (This suggests that the emacs mode might also not be able to handle having multiple files in the directory which don't compile, and trying to fix one of them?)

view this post on Zulip Scott Viteri (Apr 25 2021 at 17:10):

(deleted)

view this post on Zulip Scott Viteri (Apr 25 2021 at 17:11):

Jason Gross said:

How do I restart the language server client?

M-x lsp-workspace-restart


Last updated: May 07 2021 at 12:15 UTC