Zulip Chat Archive

Stream: new members

Topic: infoview vs goal


view this post on Zulip Nicolò Cavalleri (Jul 09 2020 at 09:38):

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

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 09:42):

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

view this post on Zulip Nicolò Cavalleri (Jul 09 2020 at 09:44):

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

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 09:45):

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

view this post on Zulip Nicolò Cavalleri (Jul 09 2020 at 09:49):

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

view this post on Zulip Nicolò Cavalleri (Jul 09 2020 at 09:50):

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

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 09:50):

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

view this post on Zulip Nicolò Cavalleri (Jul 09 2020 at 09:52):

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

view this post on Zulip Johan Commelin (Jul 09 2020 at 10:00):

Are you sure you did not type leanproject up?

view this post on Zulip Johan Commelin (Jul 09 2020 at 10:00):

What is the content of your leanpkg.toml?

view this post on Zulip Johan Commelin (Jul 09 2020 at 10:01):

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.)


Last updated: May 18 2021 at 17:44 UTC