VSCODE outline mode not working in imports

Stream: new members

[Richard L Ford]

When I have a project that imports the mathlib, the vscode outline extension works in my own files, but when I use goto-definition to something in the math library, in that file, the outline is not showing. Instead there is a message saying "no symbols found in document <filename>". I had setup the project using lake in the recommended way for projects using the mathlib. As an example, if I checkout the mathematics in lean repo, the outline works fine in its files, but not those in the .lake subdirectory. When I had cloned the repo, I had then done:

lake exe cache get
lake build

Is there something else I should do?
I also experimented with trying to build the mathlib that was below in .lake/packages, but that did not seem to help.

[Marc Huisinga]

I can reproduce this, even for files within the same project. Breadcrumbs and other language server navigation features for that file are not available either. I've checked that the language server receives the request and responds to it appropriately, but for some reason VS Code decides to not display the result. I'll have to do some deeper debugging of this issue.

[Marc Huisinga]

I'm now fairly confident that this is a VS Code bug (not an LSP language client library bug). One shoddy workaround is to add a line to the document you're looking at and then deleting it. This seems to make VS Code refresh the outline view when the document is fully processed.

[Eric Wieser]

I think we looked into this in the past for Lean 3, and it was something like the outline view request coming in long before the Lean file had been processed

[Marc Huisinga]

Eric Wieser said:

I think we looked into this in the past for Lean 3, and it was something like the outline view request coming in long before the Lean file had been processed

"Processing a file" is a language server notion and the Lean 3 and Lean 4 language servers couldn't possibly be more different. The server does the right thing here and provides the result when the file has been fully processed, VS Code just doesn't render it. I'll have to do some VS Code debugging tomorrow to figure out why.

[Richard L Ford]

@Marc Huisinga, thanks for the workaround! That works for me.

[Marc Huisinga]

I managed to find and fix this issue and a new vscode-lean4 version containing the fix will be released soon.
If you're curious about the details: vscode-lean4#460

[Richard L Ford]

@Marc Huisinga Thanks for fixing this!