Minor UX quibble

Stream: iris-lean

[Shreyas Srinivas]

Could we get syntax highlighting in the infoview for Iris declarations as well? What would we have to do to get this? Currently we use the delaborator in Iris.Proofmode.Display. Or better yet, something fancier using proofwidgets?

[Mario Carneiro]

can you show a screenshot of what you mean? I already get syntax highlighting for a lot of things in the proof mode

[Shreyas Srinivas]

Screenshot from 2025-07-17 17-05-48.png

[Shreyas Srinivas]

from the example file

[Mario Carneiro]

I will note that there is a gap in the capabilities of customizing the goal view, which is why you get this funny double turnstile thing

[Mario Carneiro]

I would like to have something like the old begin[iris] mechanism from lean 3, but it's not really possible to do this today. You can have a by_iris which takes iris_tactic syntax but you can't create alternatives to the goal view without losing a lot of functionality

[Shreyas Srinivas]

Can't we extend the delaborator to tell it to highlight somethings in a different colour on the infoview?

[Mario Carneiro]

in short, this is something that iris-lean does not have the power to fix, you need to bug lean core devs to fix it

[Mario Carneiro]

no, highlighting is not under control of delaborators

[Mario Carneiro]

cc: @Marc Huisinga

[Shreyas Srinivas]

right. then that leaves proofwidgets for now. It might be a severe misuse of proof widgets to show another goal view. But there is some precedent : #general > Display goal as LaTeX in infoview @ 💬

[Shreyas Srinivas]

More specifically this : #general > Display goal as LaTeX in infoview @ 💬

[Shreyas Srinivas]

even an HTML display of the iris goal view would be cleaner than what we have, minus some interactive functionality

[Mario Carneiro]

a widget goal view is certainly an option, but it shows in addition to the regular goal view, and we have to play catch-up with the features of the regular mode. I would much rather have an approved way to do this

[Shreyas Srinivas]

@Marc Huisinga : can we anticipate major changes in the infoview in the coming months?

[Shreyas Srinivas]

If not then maybe it is worth it to have a proofwidgets substitute for a while

[Michael Sammler]

Please keep in mind that proof widgets do not work in all editors. (In particular, they do not work in Emacs and need to be manually reimplemented in nvim AFAIK.) So there should always be a version of the goal display that does not require proof widgets.

[Shreyas Srinivas]

It won’t replace it. It will just augment it until the infoview gets extensibility. Maybe I should have used the word “augment” instead of “substitute”, since proofwidgets can’t affect the goal view either.

[Markus de Medeiros]

I like the Iris infoview as it is honestly. It's already less visual clutter than Rocq Iris which I am used to haha.

[Markus de Medeiros]

I'm glad we (the royal we, meaning Mario) got rid of those gigantic horizontal lines

[Oliver Soeser]

I am very averse to the infoview becoming any more cluttered than it needs to be, but I guess this could be a nice add-on for those who'd benefit from it?

[Markus de Medeiros]

One step closer to the Iris video game...

[Shreyas Srinivas]

1. The infoview changes that Mario is proposing would give us the colourful highlighting we get for pure propositions already. We could do better than what we have now.

2. The latexified version is triggered with a tactic in lean and appears under the infoview. The second link I sent in this chat is a good example of what I have in mind, minus the fancy math rendering.

[Oliver Soeser]

Colourful highlighting would be nice yes

[Shreyas Srinivas]

That and the ctrl click and (subt)-term highlighting on mouse over

[Shreyas Srinivas]

We are essentially just rendering text.

[Shreyas Srinivas]

Hovering the mouse over the iris proof view highlights the whole thing. Not the individual subterms. It doesn’t even separate the hypothesis and goal

[Shreyas Srinivas]

Ideally we could have all of this appear in the infoview and the iris hypothesis could get highlighted in a custom colour

[Mario Carneiro]

just to clarify the changes I would like to see: the iris tactic mode goal state would look exactly like the current one, except that hypotheses would be above the turnstile and treated exactly like regular hypotheses, including the highlighting and the greying out for inaccessible or shadowed hypotheses, but with boxes and stars before them to indicate that they are persistent or spatial hypotheses

[Shreyas Srinivas]

For iris users' convenience, I think some visible difference between Iris props and pure declarations/props is still useful to have

[Mario Carneiro]

they already have a visible difference, this is the star/box you can see in the screenshot