VSCode checking and tooltips

Stream: new members

[Roman Fedorov]

VSCode stopped continuously checking the lean files. I am able to re-check with Shift-Ctrl-X though it is very slow. I am also not getting tooltips when I point my cursor to an element. Any ideas of how to fix it? I am working with Lean4.

[Alex J. Best]

If you restart lean (or vscode) does the problem persist?

[Scott Morrison]

If the problem persists after restarting VSCode, you should go to the command line as see if lake build is rebuilding everything. If it doesn't terminate quickly, try instead lake exe cache get && lake build to download precompiled oleans.

[Roman Fedorov]

@Scott Morrison , thank you, I tried both commands and the problem persists

[Roman Fedorov]

@Scott Morrison to make it precise, I have a file test.lean consisting of a single line #eval 3+7. If I change the numbers it would not recalculate.

[Scott Morrison]

Just making sure it is really a single line: no imports or anything?

[Roman Fedorov]

@Scott Morrison A single line.

[Scott Morrison]

I'm sorry, I haven't seen anything like this, and could only suggest starting to uninstall and reinstall various components (delete your ~/.elan directory, reinstall elan, etc)

[Roman Fedorov]

Uninstalling everything did not help. I made a new account and installed lean4 there. It worked for a while but then I updated mathlib4 and it stopped working. The current state is: I am trying to build Data.Fin.Basic and I am getting lots of mistakes (in particular, that something has already been defined in Std.Data.Fin)

[Alex J. Best]

How did you update mathlib4? This sounds like a mismatch between mathlib and std versions which should be handled by lake only. Are you working on mathlib or your own project?

[Roman Fedorov]

I updated by running "lake update" from the Mathlib directory. Formally speaking, I am working on my own project.

[Sebastian Ullrich]

Please see the note at https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

[Roman Fedorov]

Thanks, I tried running the commands. When I run "lake exe cache get", I get a message ... Downloaded 0 file(s) [attempted 3470/3470] 0% success. Also, the page says: "Make sure that your project uses the same Lean 4 toolchain as the one used in mathlib4" but it does not say what to do when this is not the case.

[Sebastian Ullrich]

That is what the curl command does, which is explained further above

[Sebastian Ullrich]

Did you revert your changes in the mathlib4 directory first?

[Roman Fedorov]

Thanks. It was easier just to restart the project in a new directory. It works now.