lean4-mode emacs issues

Stream: lean4

[Jason Gross]

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

[Julian Berman]

(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)

[Jason Gross]

How do I restart the language server client?

[Julian Berman]

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)

[Jason Gross]

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?)

[Scott Viteri]

(deleted)

[Scott Viteri]

Jason Gross said:

How do I restart the language server client?

M-x lsp-workspace-restart