Goto references does not work for stray files

[lovettchris]

Goto references on "foo" doesn't jump to the line of code in bar that is referencing foo.

def foo : Nat := 10

def bar : Nat := foo * 10

#eval bar

[gebner]

I think go-to-references only works with lake serve iirc.

[Kha]

For references to work the file must be both a physical file (according to DocumentUri.toPath?) and in the LEAN_SRC_PATH (which lake serve should set to include the current project (if any), yes). @Garmelon I wonder if it would be better to index ileans not by module name but by file URI in the watchdog in order to lift these restrictions. For opened files this seems natural as LSP identifies files in this way. For closed files, we would have to move the "does this .ilean file actually have a corresponding .lean file" check from request time to load time. Which should also reduce the I/O ops you observed for requests. Do you see any issues or downsides with this change?

[Kha]

Independently, we might eventually want to implement the references request in the file worker as well as a fallback (as is the case for definitions), which would solve this as well. This would be required even after the above change to also handle the request on local binders (say, where/mutual decls) correctly. That's not high priority I'd say, but would be nice to have eventually for consistency.

[Garmelon]

I wonder if it would be better to index ileans not by module name but by file URI in the watchdog in order to lift these restrictions.

This should work as long as modules aren't moved from one path in LEAN_SRC_PATH to another, but the current system already doesn't expect multiple ileans for the same module, so I don't expect this to be a problem. Also, this could be solved if ileans stored a relative path to their lean files instead of a module.

Do you see any issues or downsides with this change?

Re. moving checks to load time: Deleting or moving lean files while the server is already running could lead to the server responding with nonexistent file urls. VSCode will complain about files it can't open. The server should probably still check if lean files exist before every reply.

[Garmelon]

This would be required even after the above change to also handle the request on local binders (say, where/mutual decls) correctly.

Why? Aren't those just local identifiers? I thought those already worked using the current system.

With the change of indexing ilean info via file URL, this fallback shouldn't be needed, I think.

[Kha]

Ah right, it's only the .ilean files that are missing local references, not the worker->watchdog updates.

[Kha]

but the current system already doesn't expect multiple ileans for the same module, so I don't expect this to be a problem. Also, this could be solved if ileans stored a relative path to their lean files instead of a module.

Yes, this should be fine. And let's not add additional resolution systems on top of LEAN_SRC_PATH unless necessary.

The server should probably still check if lean files exist before every reply.

Yes, but at least we don't have to search through LEAN_SRC_PATH anymore for every matching file.

[Garmelon]

The search through LEAN_SRC_PATH for each file is less expensive than resolving the resulting path into an absolute path for the file URL, from what I can tell. Avoiding LEAN_SRC_PATH might not change much.

Edit: On my machine, both take on the order of 10 microseconds per file, with the call to IO.FS.realPath taking a few microseconds longer than the call to Lean.SearchPath.findModuleWithExt according to timeit. I don't have a very complicated LEAN_SRC_PATH though, so this may vary from setup to setup. Also, I don't know how the situation is on windows.