Zulip Chat Archive

Stream: new members

Topic: goal window disappeared

Robert Watson (Feb 10 2022 at 15:44):

Hi there, how do I reopen my goal window for a Lean 4 file in VS Code? When I open the file and look at Infoview it does no type checking. It says no info found, all messages (0) ...

Joachim Breitner (Feb 10 2022 at 15:52):

So the window (on the VS Code sense) is still there. Did you do something, like pulling mathlib master? (Then maybe you have a version mismatch between lean and mathlib)

Robert Watson (Feb 10 2022 at 15:59):

It's there because I closed and reopened VSCode, the folder and the file. I don't think i did anything to mathlib. It's a new install anyway, and was type checking just fine before. Maybe VSCode got updates automatically or something?

Joachim Breitner (Feb 10 2022 at 17:00):

Does it say “loading” or something like that?

Joachim Breitner (Feb 10 2022 at 17:01):

Oh, lean4. I don't think I can contribute any useful debugging then :-)

Robert Watson (Feb 10 2022 at 17:09):

No it doesn't. I guess I have to just redownload the folder I'm using. Thanks anyway.

Last updated: Dec 20 2023 at 11:08 UTC