New Lean 3 files do not seem to work (with the LSP) until reopened about lean.nvim HOT 8 CLOSED

I got a few minutes just now to look at this a bit -- pretty sure the issue is here where we use root_pattern to try to find the project root -- but that returns nil when the file itself doesn't exist (which seems to be here, simply because fs_realpath will return nil).

The LSP config instead has some fallback logic for that case.

Lean 4 works just because yeah that's what we set when we don't detect Lean 3.

from lean.nvim.

(will likely revert f182bda once neovim/nvim-lspconfig#1041 is resolved/merged)

from lean.nvim.

For me writing and reopening doesn't make it work either -- curious how you managed that.

The issue here is that standalone Lean buffers are assumed to have the lean (Lean 4) filetype by default - so for now doing something like :set ft=lean3 should get things at least partially working.

The real solution is to update the require('lean.lean3').init() function (with its outdated use of the vim.b.lean3 variable) to tear down any Lean-4 related stuff and properly re-init with the lean3 filetype. I've mistakenly been ignoring this throughout our refactors :/

Will make a fix along with a unit test soon!

from lean.nvim.

So, actually I think we should just rely on something like a modeline for Lean version inference in this case. IMO standalone Lean 3 files are enough of an edge case that it's not worth the additional code for dynamically switching from Lean 4 to Lean 3 in a single file. And I believe in any case you would have to do elan default "leanprover-community/lean:3.30.0" before opening the file, assuming your current default is Lean 4.

So I'm thinking we could just parse something like:

-- ft=lean3

at the beginning of a standalone Lean 3 file to override the default standalone filetype of lean with lean3.

@gebner CMIIW but it looks like VSCode doesn't support any kind of Lean 3 vs. Lean 4 inference for standalone files like this either? Perhaps this modeline is something we could standardize between the editors? Or maybe if a modeline is inconvenient we can support a .lean3 filetype extension?

from lean.nvim.

ACTUALLY I see what's being done at VSCode is you're parsing the output of lean --version to determine the filetype, which is frankly what we should be doing instead of parsing leanpkg.toml.

from lean.nvim.

Will fix ft.lua to do this, only falling back to the existing method if it first determines that elan is not installed.

But still, would seem convenient to have some way to avoid having to do elan default ... to switch back and forth between Lean 4/Lean 3 when working with standalone files, maybe a modeline or .lean3 extension would be part of the solution? Though I can tell this probably isn't a very high priority item. Let me know your thoughts.

from lean.nvim.

This very well may have something to do with my setup, I haven't investigated yet, but this bug was about properly specc'ed Lean 3 buffers (i.e. not standalone files).

For me, when I open a new Lean 3 file, I get no LSP, whereas for a Lean 4 file, or an existing Lean 3 file, it works fine.

Demo:

What behavior do you see when:

• opening a new Lean 3 file in a project with a leanpkg.toml specifying lean 3?
• opening an existing Lean 3 file in that same project
• opening a new Lean 4 file in a project with a leanpkg.toml specifying lean 4?

Is it different than mine above? (Feel free also to let me figure out whether this is my fault or not with my local setup)

But we can't do anything like a modeline or changing extension without upstream support (which I doubt we'd get, there's too much existing lean 3 code out there), so I wouldn't think too hard about that part.

from lean.nvim.

Just fixed - though this also reveals a problem with the root directory search in nvim-lspconfig: see neovim/nvim-lspconfig#1045.

from lean.nvim.