small "37 goals" message

Stream: lean4

[Kevin Buzzard]

In Lean 3 there was a little message at the top of the tactic state saying the number of goals currently in the infoview, if there was more than one. Can I turn that option on in Lean 4?

[Heather Macbeth]

I miss this too.

[Heather Macbeth]

While we're on infoview tweaks: I'd love to have options to adjust the infoview by

1. hiding the autogenerated "case names" for the goals
2. leaving a fair bit of whitespace between the different goals
3. hiding the "expected type"

Do these already exist?
Screen-Shot-2023-04-25-at-10.38.15-AM.png

[Heather Macbeth]

Maybe even

4. make the text of the subsequent goals smaller than the text of the current goal.

[Ruben Van de Velde]

Sounds like you have the same issue I have with finding the current goal - maybe it would be possible to auto-collapse all but the first goal states

[Heather Macbeth]

Not so much me as my poor students :). I'd rather not autocollapse it, because I think that would confuse them further, but I think the tweaks I proposed would make it clearer.

[Sebastian Ullrich]

Heather Macbeth said:

3. hiding the "expected type"

Not that if you collapse any part of the info view, it should stay collapsed for the current session. Is this visually sufficient? Should it persist across sessions? Adjustable in your project's .vscode file?

[Heather Macbeth]

Adjustable in your project's .vscode file?

I think that would work, yes -- I'd rather my students never see this at all.

[Kevin Buzzard]

But you want them to see the number of goals, right? :-)

[Heather Macbeth]

Yes -- it's the "expected type" that I want them to never encounter. I do want them to see all the goals, and I'd love for them to see a count of the number of goals.

[Heather Macbeth]

(See the picture I included as an illustration of why "expected type" can be confusing.)

[Patrick Massot]

It would be even better to make the active goal clearly designated than being on top.

[Heather Macbeth]

Yes, maybe it could even have a lightly coloured background instead of/in addition to

Heather Macbeth said:

4. make the text of the subsequent goals smaller than the text of the current goal.

[Patrick Massot]

Oops, I missed your 4th item. But this shows I had the same wish (although I don't know which display trick would be the most suitable).

[Sebastian Ullrich]

For what it's worth, for cases like above where presumably the expected type is the type of the surrounding by block, we probably shouldn't ever show an expected type. As everywhere, there is so much more that could be tweaked and improved, but an option to collapse the item by default would be a sensible start.

[Yaël Dillies]

Patrick Massot said:

It would be even better to make the active goal clearly designated than being on top.

"active goals". There can be several active goals, right?

[Yaël Dillies]

I guess students don't use much ; (<;> is the Lean 4 equivalent, I think?), but it would still be helpful to display all the goals the next tactic will run on.

[Heather Macbeth]

Sorry for hijacking your thread, Kevin. I agree about the importance of the "37 goals" message, too.

[Heather Macbeth]

@Sebastian Ullrich I'd be happy to open issues for these, totally understanding that they are lower priority for the devs than work on the core product and these issues would just be a record. But could you give a run-down of which repo each of these ideas (my 1-4 and Kevin's "number of goals") would require changes to? Are they all VS Code-extension only, or do some require changes to core too?

[Sebastian Ullrich]

I just opened https://github.com/leanprover/lean4/issues/2202, I believe everything else can be done in the extension, including a setting to collapse the expected type by default

[Sebastian Ullrich]

Yaël's refinement may need some coordination between language server and extension, in which case I would default to opening it in the lean4 repo

[Sebastian Ullrich]

And yes, right now I don't think anyone is directly looking into working on issues like these in either repo, but recording them is still useful

[Patrick Massot]

I opened https://github.com/leanprover/vscode-lean4/pull/300 which seems to be the easiest vscode-lean4 issue to fix.

[Kevin Buzzard]

I was wishing for this only today, after it had taken a while to dawn on me that an apply in a porting file was creating two goals in lean 4 and only one in lean 3

[Patrick Massot]

There is a failing test but I have no idea what it's telling me.

[Wojciech Nawrocki]

@Patrick Massot I will review. The failing test says nothing, the tests have been broken for ages.

[Patrick Massot]

Thanks to two TGV rides between Paris and Lyon, I found time to work on https://github.com/leanprover/vscode-lean4/pull/302 which tries to implement all suggestions from Heather's VSCode wishlist. However I'm facing some React issues. I added some config options here which are made available here using what I understand to be the standard procedure in this extension. Then they are read for instance here and some of them are used as the initial state of some React state, for instance here. That doesn't work. I think what happens is the config passing mechanism is asynchronous and the react component state is initialized before the config goes through. And then it's too late. Please feel free to fix that or give me hints @Gabriel Ebner @Wojciech Nawrocki @Edward Ayers

[Patrick Massot]

Also I apologize for implementing four different features in the same PR, but writing all four at the same time was much easier for me since the work is mostly threading variables through all layers, so working one layer at a time is easier than one variable at a time. Of course I can try to split the PR if this is really too annoying.

[Patrick Massot]

Once the config vs state issue is resolved we will of course be able to enjoy some bikeshedding about the changes of margins and font-size, and the default keybindings.

[Wojciech Nawrocki]

Thanks! I will try to look at this tonight.