Autostart LSP for Lean 4 standard library files and make Lean 3 standard library filetype detection more robust.

[rish987]

For Lean 3 I was getting a path like .../.elan/toolchains/leanprover-community--lean---3.31.0/lib/..., (yes 3 hyphens after lean) so I think this would be a better catch-all.

And for Lean 4 CMIIW but I don't think the server started at all for standard library files before? In Lean 3 the root finder from nvim-lspconfig found the init folder, but things are structured differently in Lean 4, so this didn't seem to work at all. Figured this was a simple enough way to do it, but of course suggestions welcome. In case you're wondering how VSCode does it, I believe it associates servers with workspaces, which are collections of (gross) UI elements, as opposed to nvim which uses root directories.

[codecov[bot]]

Codecov Report

Merging #116 (0e03bd9) into main (d63c183) will increase coverage by 0.01%. The diff coverage is 100.00%.

@@            Coverage Diff             @@
##             main     #116      +/-   ##
==========================================
+ Coverage   94.30%   94.31%   +0.01%     
==========================================
  Files          31       31              
  Lines        1685     1690       +5     
==========================================
+ Hits         1589     1594       +5     
  Misses         96       96              

Impacted Files	Coverage Δ
lua/lean/lean3.lua	95.23% <100.00%> (ø)
lua/lean/lsp.lua	63.82% <100.00%> (+4.30%)	:arrow_up:

---

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update d63c183...0e03bd9. Read the comment docs.

[Julian]

For Lean 3 I was getting a path like .../.elan/toolchains/leanprover-community--lean---3.31.0/lib/..., (yes 3 hyphens after lean) so I think this would be a better catch-all.

Sounds good.

And for Lean 4 CMIIW but I don't think the server started at all for standard library files before?

It definitely works here, but my setup is undoubtedly different than yours, I don't have elan.

nvim has workspace folders too AFAIK, they're part of the LSP spec (see e.g. :h vim.lsp.start_client which is what nvim-lspconfig calls). But yeah maybe we need a fix upstream? What root_dir is yours detecting, and is this when directly editing a stdlib file or when jumping to a definition within a stdlib file or both? What's here doesn't seem the right way to fix an issue there to me, textDocument/definition isn't really special, it's just one of many operations, so if the client isn't starting up we should fix it in the detection logic.

[gebner]

FWIW, go-to-definition to the Lean 4 standard library works for me (and I use elan). What doesn't work is if I use go-to-definition in mathlib to go to the standard library, or open nvim in the lean checkout. (The detection code should probably check for leanpkg.path in addition to leanpkg.toml.)

This PR seems to break Lean 3 support completely. Mathlib is now detected as Lean 4.

In case you're wondering how VSCode does it

The vscode extension is from a time before workspaces, when there was only one root directory. The extension just starts the server in the root directory. Finding the correct directory is left as an exercise to the user.

[Julian]

Interesting, thanks.

What doesn't work is if I use go-to-definition in mathlib to go to the standard library

Assuming you don't mean mathlib4 there this works for me so will have to check what could be different (I know at least that my fake-elan has lean 4 set as the default, so maybe that?), but:

open nvim in the lean checkout

If this is again lean and not lean4's repo then this indeed doesn't work for me I see (I hadn't checked before). Is there even a way we can detect this is lean3, or would we have to just special case?

(The detection code should probably check for leanpkg.path in addition to leanpkg.toml.)

I don't follow what we should read out of leanpkg.path (or is this to populate workspace folders?)

[gebner]

What doesn't work is if I use go-to-definition in mathlib to go to the standard library

Assuming you don't mean mathlib4 there this works for me so will have to check what could be different (I know at least that my fake-elan has lean 4 set as the default, so maybe that?), but:

I meant the Lean 3 mathlib. If I use go-to-definition on anything that leads to the standard library, nvim will open the correct file but it is incorrectly detected as the lean filetype (i.e., Lean 4).

open nvim in the lean checkout

If this is again lean and not lean4's repo then this indeed doesn't work for me I see (I hadn't checked before). Is there even a way we can detect this is lean3, or would we have to just special case?

(The detection code should probably check for leanpkg.path in addition to leanpkg.toml.)

I don't follow what we should read out of leanpkg.path (or is this to populate workspace folders?)

These two are related. The leanpkg.path file tells us that 1) this is a Lean 3 project, and 2) where we need to start the server. (The core Lean 3 library only has a leanpkg.path file but not leanpkg.toml.)

[Julian]

I see. OK -- I didn't realize leanpkg.path was gone entirely in lean4, my mathlib4 had a leanpkg.path file in it, probably from me mistakenly running a Lean 3 leanpkg in it at some point.

[rish987]

It definitely works here, but my setup is undoubtedly different than yours, I don't have elan.

nvim has workspace folders too AFAIK, they're part of the LSP spec (see e.g. :h vim.lsp.start_client which is what nvim-lspconfig calls). But yeah maybe we need a fix upstream? What root_dir is yours detecting, and is this when directly editing a stdlib file or when jumping to a definition within a stdlib file or both? What's here doesn't seem the right way to fix an issue there to me, textDocument/definition isn't really special, it's just one of many operations, so if the client isn't starting up we should fix it in the detection logic.

When I go-to the definition for Or, for example, it takes me to elan's lib/lean/src/Init/Prelude.lean, and there's no leanpkg.toml anywhere here, so lspconfig just uses the current directory (Init). Then, when it tries to initalize from there, the server doesn't respond to the initialize request, so the buffer is left without an LSP client. Did you see a new client being created when you entered a stdlib file, or did it keep the same one you had from mathlib (before this PR)?

[rish987]

@gebner Is it possible to patch elan to correctly infer lean version within its own downloaded stdlib files? If so then, along with a fix for #88 (that gets the filetype from lean --version) we could do away with this fragile regex matching. Note that lean filetype is the default, so if this breaks things for you it means that our Lean 3 pattern didn't match -- what is the path that your Lean 3 stdlib files are in?

[gebner]

what is the path that your Lean 3 stdlib files are in?

• /home/gebner/.elan/toolchains/leanprover-community--lean---3.31.0/lib/lean/library/ (which unfortunately doesn't even have a leanpkg.path file)
• /home/gebner/lean/library/

Is it possible to patch elan to correctly infer lean version within its own downloaded stdlib files?

I didn't realize that this was an issue, how does this even work right now? When I go to the library directory, then lean just fails:

$ cd .elan/toolchains/leanprover--lean4---nightly-2021-08-16/
$ lean
error: no default toolchain configured. run `elan default stable` to install & configure the latest Lean 3 community release.

Nevertheless, go-to-definition to the standard library works just fine (in Lean 4).

[rish987]

Yeah I see the same, in my case it just uses the default toolchain that I have set (lean 3 at the moment).

Go-to definition I would expect to work fine, the problem is (for me at least, and I have a standard setup, haven't really tweaked anything) an LSP client is never attached. For example do you get anything in the table from :lua print(vim.inspect(vim.lsp.buf_get_clients(0))) after go-to definition to Lean 4 stdlib?

[gebner]

Go-to definition I would expect to work fine, the problem is (for me at least, and I have a standard setup, haven't really tweaked anything) an LSP client is never attached. For example do you get anything in the table from :lua print(vim.inspect(vim.lsp.buf_get_clients(0))) after go-to definition to Lean 4 stdlib?

Surprisingly, the LSP client is attached just fine. Here are the presumably relevant lines from the output of that command:

      cmd = { "lean", "--server" },
      root_dir = "/home/gebner/.elan/toolchains/leanprover--lean4---nightly-2021-08-16/lib/lean/src/Lean/Util",
    workspaceFolders = { {
        name = "/home/gebner/.elan/toolchains/leanprover--lean4---nightly-2021-08-16/lib/lean/src/Lean/Util",
        uri = "file:///home/gebner/.elan/toolchains/leanprover--lean4---nightly-2021-08-16/lib/lean/src/Lean/Util"
      } },

[rish987]

Thanks. In my case I just don't get any new client like you do, I've traced it a bit and it looks like the server didn't respond to the initialize request, also in that case we don't set cwd so I'll need to look a bit more into what's going on with uv.spawn when cwd = nil. So something weird may be going on for my setup, though I can't really think of anything I've changed.

[rish987]

Ah yes so it seems that uv.spawn assumes the current directory when cwd = nil, so that makes whether or not this will work for you dependent on which particular directory you're in, which is no bueno. I'd assume you're doing things from the mathlib4 directory, or some other lean project directory, it works for me as well when I do nvim from there, but not when I open the same mathlib file from some random directory. So there's a bit of a different fix needed here, possibly in nvim-lspconfig.

[Julian]

When I go-to the definition for Or, for example, it takes me to elan's lib/lean/src/Init/Prelude.lean, and there's no leanpkg.toml anywhere here, so lspconfig just uses the current directory (Init). Then, when it tries to initalize from there, the server doesn't respond to the initialize request, so the buffer is left without an LSP client. Did you see a new client being created when you entered a stdlib file, or did it keep the same one you had from mathlib (before this PR)?

Just to throw what I see in again -- if I:

• create a file called foo.lean in a random directory (my home directory below)
• type #check Or into it
• goto definition

before this PR I get I believe correct behavior, a new client. LspInfo in the new stdlib buffer shows me:

1 client(s) attached to this buffer: leanls

  Client: leanls (id: 2 pid: 15092)
    root:      /opt/lean4/nightly/lib/lean/src/Init
    filetypes: lean
    cmd:       lean --server
    autostart: True

2 active client(s): 

  Client: leanls (id: 1 pid: 15088)
    root:      /Users/julian
    filetypes: lean
    cmd:       lean --server
    autostart: True

  Client: leanls (id: 2 pid: 15092)
    root:      /opt/lean4/nightly/lib/lean/src/Init
    filetypes: lean
    cmd:       lean --server
    autostart: True

Clients that match the filetype lean:

  Config: leanls
    cmd:               lean --server
    cmd is executable: True
    identified root:   /opt/lean4/nightly/lib/lean/src
    autostart:         True
    custom handlers:   $/lean/plainTermGoal, $/lean/plainGoal

(Maybe tracking the list of scenarios will help? It'd definitely help me -- the two I think I see are making lean 3 repo checkout files work, which requires using leanpkg.path marker files, and then also yeah making files within elan toolchains themselves work)

[rish987]

Yeah, so it had to do with my elan default being Lean 3, it works just like you describe when it's Lean 4. Also a new client for every single stdlib directory seems less than ideal, shouldn't we make it so that every stdlib buffer shares the same client (with root lib/lean/src)?

[Julian]

Yeah, so it had to do with my elan default being Lean 3, it works just like you describe when it's Lean 4.

Aha cool, progress!

Also a new client for every single stdlib directory seems less than ideal, shouldn't we make it so that every stdlib buffer shares the same client?

Yes agree if we can find a way to detect this -- seems nontrivial though possibly no? I don't see an easy marker that tells you where the root dir of the installation starts, unless you just pick some well-known file to look for like src/Init/Prelude.lean and walk upwards looking for it? Or maybe doing it just for the 90% case (where someone's installed via elan) is easier as well? At least there you can ask elan where the root is.

But we should prioritize things that don't work over making things faster I think as well.

[rish987]

Agreed, so what doesn't work here seems to be simultaneous support of Lean 3/Lean 4 stdlib LSP. The changes needed I think are twofold:

1. Modify upstream nvim-lspconfig's leanls to be able to fall back to lib/lean/src as a root.
2. Patch elan to be able to correctly infer lean --version to be Lean 4 within lib/lean/src. @gebner @Julian let me know how reasonable this sounds. We can also do similar for lean3ls so that the elan default ... version is truly irrelevant for stdlib files.

[gebner]

Patch elan to be able to correctly infer lean --version to be Lean 4 within lib/lean/src.

Is this what you were thinking of? https://github.com/leanprover/elan/pull/36

[rish987]

Yes exactly that, thank you! Though you've given me another excuse to put off learning Rust for a bit XD

[rish987]

Closing in favor of #119, neovim/nvim-lspconfig#1156