Filter : only props won't stick

Stream: general

[Kevin Buzzard]

I have just discovered the brilliant filter : only props on VS Code which I think will be really helpful for beginners in my class tomorrow. But whenever I type in another tactic it switches back to "no filter".
Can I somehow stop this happening?

[Bryan Gin-ge Chen]

Ah, I think the widget mode filters don't have persistent settings associated to them. This probably wouldn't be too hard to add, but I'm a bit swamped at the moment.

Would the text mode filters work for you?

[Bryan Gin-ge Chen]

Wait, nevermind. There's no good way to filter for only props with the text mode tactic state.

[Bryan Gin-ge Chen]

Hmm, the filter dropdown is written in Lean (here's the mathlib version and here's the core Lean version). Unfortunately, I don't have enough experience with Lean widgets yet to know how to make that setting persist. Maybe some of the widget superstars in your Discord could help?

[Kevin Buzzard]

I'll ask around! If I wanted to open this as an issue, which repo does it get filed under? When dealing with a composite of G-module homs I have seven instances to deal with and they're clogging up the fun part. I'm sure the analysts must have run into this

[Mario Carneiro]

This probably requires changes in the lean repo

[Mario Carneiro]

the vscode extension may also need to participate

[Kevin Buzzard]

It's a really nice way of setting lean into "proof mode" when all definitions are done. Students filling in sorrys in my course might be tempted to always keep instances off for the entire workshop if this were possible because they always know that G is a group and that M, N, P are G-modules

[Bryan Gin-ge Chen]

Pinging @Edward Ayers :pray:

[Edward Ayers]

Yeah this is in my todo list but I think it would require some fiddling with core lean

[Edward Ayers]

It's a core lean issue. A quick mathlib fix would be to add an option that the filter widget then reads.

[Kevin Buzzard]

There was a minor riot in the class when they all discovered this cool "only display the maths" option and then found that it didn't stick!

[Filippo A. E. Nuccio]

@Kevin Buzzard Kevin, did you finally find a way to "freeze" the Infoview to only props?

[Kevin Buzzard]

No, I just completely forgot about the problem

[Kevin Buzzard]

I just had a polite British whinge and then shut up, that's what i usually do :-)

[Kevin Buzzard]

or maybe I did and then forgot about the solution

[Filippo A. E. Nuccio]

I see, I am just fighting against my screen which does not fit the seventeen instances I have..

[Kevin Buzzard]

I can confirm that my laptop's only props is not sticking, but in plain text mode (non-widget) "goals only" sticks.