lsp seems to get out of sync with actual document (often)

Stream: lean4

[MangoIV]

Hi; I'm having the issue, that my lsp gets out of sync very often with the actual documents; I'm using a mathlib commit from yesterday and the respecting toolchain; the lean plugin is the newest nvim plugin; this is a new issues, I didn't have it with different toolchains.

image.png

[MangoIV]

attached is a screenshot of how it looks; I've also had some issues about the LSP not recognising things like .S anymore after making a typo and having to restart the LSP

[MangoIV]

also very often the LSP just gets stuck on "Processing"

[Marc Huisinga]

For how long have you been experiencing these issues? The Mathlib toolchain is three weeks old at this point.

[MangoIV]

I've been experimenting with lean on and off, these issues are new in the project I just started experimenting with.

[Marc Huisinga]

Do you encounter the same issue with VS Code?

[MangoIV]

I can try codium; I can also try a project with an older toolchain

[MangoIV]

for codium it just tells me "the lean server has stopped processing this file [..] likely due to a stack overflow or a bug", when trying to use \ to write a unicode symbol; maybe I'm doing something wrong here; what things have to be in sync?

• I have lean4 and lake from the release candidate specified in the toolchain file
• I have everything else installed via lake
• mathlib is the latest master from yesterday

[MangoIV]

ah no this only happens when trying to add an arrow behind an existing arrow in an inductive type (and only sometimes?)

[Marc Huisinga]

Out of curiosity, are you using a standard Lean setup? If not, then there is little that can be done to help you because the issue may be due to how you set up Lean.

[MangoIV]

I’m not using elan to manage my lean binaries because I’m not a big fan of installing things globally but it should amount to the same thing, hence my questions.

[Marc Huisinga]

It doesn't, e.g. the VS Code extension relies on Elan being present.

[MangoIV]

Alright; well I guess I’ll have to give in and accept this mess as necessary evil if I want to get lean working :melting_face:

[Kim Morrison]

If you are aware that you are using a setup significantly different than the supported one, it would be helpful to say so at the beginning of the thread, so that we can more efficiently say "please use elan". :-)

[Joachim Breitner]

Marc Huisinga said:

It doesn't, e.g. the VS Code extension relies on Elan being present.

Out of curiosity, how so?

[MangoIV]

Scott Morrison said:

If you are aware that you are using a setup significantly different than the supported one, it would be helpful to say so at the beginning of the thread, so that we can more efficiently say "please use elan". :-)

As I was trying to convey I was not aware I’m using a setup significantly different; I was only aware of elan not being present which seemed fine to me according to my understanding of what it’s supposed to do.

[MangoIV]

What elan provides works though, and I’ll roll with it I guess…

[Kim Morrison]

Good point: it is potentially surprising that the VSCode extension is relying on elan rather than a manual install.

[Marc Huisinga]

As I was trying to convey I was not aware I’m using a setup significantly different; I was only aware of elan not being present which seemed fine to me according to my understanding of what it’s supposed to do.

This is what Sebastian tried to communicate earlier. Setups without Elan see no use, so they are probably broken in ways that are difficult to diagnose.

It's also not at all clear to me that lacking Elan is the actual cause of the issues you are experiencing (the VS Code extension relying on it in places was just an example); you may also have set up your Lean versions incorrectly. It's difficult to tell because the piece of software that is supposed to enforce the invariant that the correct Lean version is being used is missing.

[Marc Huisinga]

Joachim Breitner said:

Marc Huisinga said:

It doesn't, e.g. the VS Code extension relies on Elan being present.

Out of curiosity, how so?

One example: When running the language server using the language client library without a working directory (e.g. because the file is an "untitled" file), it would use the opened workspace folder for the working directory and its toolchain, which is not what you want for such files. To fix this, the VS Code extension asks Elan for the default toolchain and uses that for "untitled" files.

There's also a couple of other uses related to the very messy code that attempts to figure out which Lean version to use (e.g. for compatibility across multiple Lean versions) or how to bootstrap Elan correctly in case it isn't installed yet. This code has fallbacks for installations without Elan, but I'm sure they never see any use and are probably broken. I want to refactor all of this messy code eventually.

[Joachim Breitner]

Hmm, ok.

My naive expectation was that VSCode just shells out to lean( and maybe lake); in elan environments, the corresponding entries in the PATH are actually all elan which then consults the toolchain, downloads and execs the right binary; and that VSCode doesn't actually care whether it’s elan doing that, and as long as the lean in the PATH happens to be the right one, all just works . And only elan looks at lean-toolchain, nothing else. Maybe too naive, though.

It seems that the roles and interfaces of elan, lake, VSCode are not as cleanly specified separated as one might possibly hope, which is probably well-known to most users, but new users (of the kind that tend to stray from the default path, like me) will have to learn first the hard way.

[Marc Huisinga]

That was my initial naive expectation, too, but it's unfortunately not true since the extension does more than run a single lean or lake invocation for the server and there is a lot of state associated with that. For example:

• Whenever you select a file, the extension must decide which language client to use (the easiest example where this is necessary are multi-root projects, but it also plays a role in other contexts), which amounts to figuring out the correct folder containing a lean-toolchain that a file lives in.
• It also detects changes to the lean-toolchain file and offers to restart the server and the client if the version changed.
• The extension also has a compatibility mode so that it doesn't mess up when both vscode-lean and vscode-lean4 are active, which currently amounts to reading the lean-toolchain file.

[Joachim Breitner]

Theory vs. practice, as usual :-)

[Mac Malone]

@Joachim Breitner Another relevant detail I remember when I was contributing some to the extension: The extension assumes that the lean/lake binaries are organized into toolchains the way elan/lean does. That is, it expects a signle root toolchain foldr (e.g., LEAN_SYSROOT) to contain the both the lean and lake binaries by default (this helps ensure they come from the same toolchain version).

[Julian Berman]

Just to address the initial question -- I see this occasionally but not often. I can say the nvim plugin doesn't care how/where you got your lean from (I happen to have a nonconventional setup myself so I know it doesn't :), it should work just fine even without elan -- though yes you certainly should share that when asking questions).

[Julian Berman]

The one thing that comes to mind that I forget what VSCode does is TextDocumentSyncKind.Incremental for textDocument/didChange -- I think in neovim we have it on. Does VSCode have that enabled?

[Marc Huisinga]

Yes, VS Code has it enabled.