feat: create .ilean files #46
Conversation
|
/cc @Garmelon |
|
AFAIR there was no opposition to this change, in which case I'll merge it soon. |
|
Apparently my method of merging this in 678863c was messy and did not get automatically caught by GitHub. Oops! |
|
@Kha Did this actually work for you? Lake now generates ilean files for mathlib4, but those don't seem to be picked up by lean at all. It doesn't even find symbols or references from the current file (neither in vscode nor neovim). |
|
As far as I know, the watchdog does not ask lake for the proper src search path (only the workers do), so I wouldn't expect it to find lake's ilean files. This would also explain why it can't find references from the current file as it can't convert the LSP file URL into a module name. |
|
Yes, see
|
|
Ah, so this depends on |
Enables workspace symbols for the Lean 4 LSP. Older versions of Lake (and Lean 4) lack a serve command, so on those we fallback to the old behavior by directly starting the LSP. Closes: Julian/lean.nvim#229 Refs: leanprover/lake#46
Enables workspace symbols for the Lean 4 LSP. Older versions of Lake (and Lean 4) lack a serve command, so on those we fallback to the old behavior by directly starting the LSP. Closes: Julian/lean.nvim#229 Refs: leanprover/lake#46
Enables workspace symbols for the Lean 4 LSP. Older versions of Lake (and Lean 4) lack a serve command, so on those we fallback to the old behavior by directly starting the LSP. Closes: Julian/lean.nvim#229 Refs: leanprover/lake#46
Together with leanprover/vscode-lean4#97, this should be sufficient to get find-all-references working. I didn't want to recompile the extension, so I tested it using
LEAN_PATH=build/lib LEAN_SRC_PATH=. codeinstead.Since .ileans are "incidental" files (and basically always desirable) that are never depended on, I assume this simple setup is sufficient. I also deduplicated the affected code a little.