infoview vs goal

Stream: new members

[Nicolò Cavalleri]

When I opened my computer today, VSCode decided to show me an "infoview" window with a lot of messages instead of one single goal, and I was wondering if there were a way to go back to a single message with just the current goal

[Kevin Buzzard]

Can't you fold away the "all messages"?

[Nicolò Cavalleri]

But then I get nothing! Maybe I lost the tactic state

[Kevin Buzzard]

The new infoview should be doubling up as both the old views. Put your cursor in the middle of a tactic mode proof to see it in action

[Nicolò Cavalleri]

Kevin Buzzard said:

The new infoview should be doubling up as both the old views. Put your cursor in the middle of a tactic mode proof to see it in action

I was doing it but something weird is happening: if I only click in the middle of a proof nothing shows up, but if I write something then the tactic state appears... It is weird because I remembered that until yesterday the window was different and I only had a simple goal without all messages or anything like that, but maybe I remember wrong

[Nicolò Cavalleri]

But at least now I found a way to get the tactic state back

[Kevin Buzzard]

Yesterday you couldn't click on something in the goal window and see its type. This is the big win

[Nicolò Cavalleri]

So was something updated yesterday? I did not update anything manually!

[Johan Commelin]

Are you sure you did not type leanproject up?

[Johan Commelin]

What is the content of your leanpkg.toml?

[Johan Commelin]

Note that VS Code might have auto-updated the lean extension. (But you need both a new version of lean, and a new version of the VS Code lean extension.)