lean4
lean4 copied to clipboard
leanprover
Goto definition not working in most of LeanInk codebase
Prerequisites
- [x] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.
Description
In VS Code, editing files like alectryon.lean I get very little goto definition support.
Steps to Reproduce
- git clone https://github.com/lovettchris/LeanInk
- code LeanInk
- open alectryon.lean go to line 129
- put cursor at column 42 in
Analysis.Tokenand press F12.
In fact, try to get F12 to work on anything in this file?
Expected behavior: Should jump to the definition of Token.
Actual behavior: Nothing.
Reproduces how often: 100%
Versions
Lean (version 4.0.0-nightly-2022-09-06, commit c769808a4e33, Release)
Additional Information
Any additional information, configuration or data that might be necessary to reproduce the issue.
Works in Emacs and VSCode without any issues for me, also with all the other things in the file.
You are right, with a fresh clone and lean-toolchain of leanprover/lean4:nightly-2022-09-06 this repro above is now working for me also. Hmmm, I was originally doing some editing in one of the files here, when everything stopped working, so I will do some more debugging and figure out a repro that exhibits this problem again.
Well after coding on this branch this afternoon https://github.com/lovettchris/LeanInk/tree/clovett/hidden_namespaces (see last couple of commits) it has happened multiple times, each time it happens, and refresh file dependencies does not fix it. Closing VS code and reopening it usually does fix it, but not always. Sometimes I have to also delete the build folder, do a clean build then launch VS code, then usually that is the final fix needed to get things back on track.
@tydeu I am wondering whether this is a Windows related issue. Have you ever experienced this problem while working on Lake?
Yes indeed, does sound like the same thing and I found the same workaround Mac mentioned there - namely, developer reload, which is essentially the same as close and restart VS code. And @leodemoura - yes I've seem the same thing editing Lake code.