Find references broken in lean core

Stream: lean4 dev

[Mario Carneiro]

For a little while now I have not been able to use the "Find references" / "call hierarchy" feature across files inside lean core. I can only assume the .ilean files are broken or misplaced in some way. Could this be related to the lakefile-for-core work @Mac Malone ?

[Mac Malone]

There is no lakefile in core yet (and I have not added any new features to for it), so no, that cannot be the cause.

[Mario Carneiro]

How does the server configuration for core get set up in the first place?

[Mario Carneiro]

I guess it must still be using the lean --server fallback

[Mario Carneiro]

running #eval IO.getEnv "LEAN_PATH" and #eval IO.getEnv "LEAN_SRC_PATH" in core files returns none, not sure if I should expect that to work

[Mario Carneiro]

I figured out the issue, cc: @Marc Huisinga . initializeWorker uses moduleNameOfFileName path none to initialize the mainModuleName, which uses IO.currentDir as the root. Because I have the lean4 repo root open in vscode, this means that src/Lean/Server/FileWorker.lean will get a main module name of src.Lean.Server.FileWorker, and this ends up in the ilean outputs, resulting in lookup failures when attempting cross-file IDE queries like Find References.

[Mario Carneiro]

it seems to be nontrivial to fix this though, because it should be using searchModuleNameOfFileName but this needs srcSearchPath and this is the result of a promise that has not yet been resolved

[Mario Carneiro]

PR'd a fix as lean4#4066

[Sebastian Ullrich]

You should follow https://lean-lang.org/lean4/doc/dev/index.html#vs-code

[Mario Carneiro]

I did use that for some time but it had other annoying behaviors, like not showing the main folder in the title

[Mario Carneiro]

...also it doesn't fix the headline issue

[Sebastian Ullrich]

That surprises me, because I use those features every day

[Mario Carneiro]

never mind, I was holding it wrong

[Mario Carneiro]

(it's still a bug though)

[Mario Carneiro]

the C++ config is broken in this workspace

[Mac Malone]

Mario Carneiro said:

I figured out the issue, cc: Marc Huisinga . initializeWorker uses moduleNameOfFileName path none to initialize the mainModuleName, which uses IO.currentDir as the root. Because I have the lean4 repo root open in vscode, this means that src/Lean/Server/FileWorker.lean will get a main module name of src.Lean.Server.FileWorker, and this ends up in the ilean outputs, resulting in lookup failures when attempting cross-file IDE queries like Find References.

Oh, I wonder if this is why go-to-def does not work in the lake directory on machine but works in Init/Lean. It may be looking for lake.Lake.*?