goal window disappeared

Stream: new members

[Robert Watson]

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]

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]

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]

Does it say “loading” or something like that?

[Joachim Breitner]

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

[Robert Watson]

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