Pre-RFC: Forcing terms to be shown in hover?

Stream: lean4

[Thomas Murrills]

Usually when you hover over a term in code, it only shows the term explicitly if it’s a constant or otherwise pretty-prints to an “atomic format” (text wrapped in invisible formatting containers, like group). Otherwise it just shows the type.

I’d like to be able to force an underlying term to be shown in cases where the term is not immediately visible.

For example, in mathlib, the tfae tactics use syntax like 2 → 3 to specify which implication should be the next goal, with the number specifying the proposition in the overall TFAE [P, Q, R, …] goal. I’d like to attach the proposition as hover to the syntax (e.g. hovering on 3 would always yield R : Prop, whatever R was.)

[Thomas Murrills]

Before I make an actual RFC, though, I wanted to check that there wasn’t some way to do this that I’m missing; but I also didn’t want to clutter this stream with threads, so I figured this thread could be the zulip RFC in the case that there is no existing way (hence “pre-RFC”).

[Kyle Miller]

It would be neat if you could see the elaborated expressions for larger terms somehow.

[Thomas Murrills]

Here are some possible implementations, just to bring this request into feasibility:

The simplest way to achieve this seems to be to add a field showTerm : Bool to TermInfo, with a default value of false (and associated changes to addTermInfo and fmtTermAndModule?).

Another approach is to use special metadata attached to the expression, then check specifically for this metadata in fmtTermAndModule?. This might be more modular and accessible to meta programmers than a flag in TermInfo, but seems like it’s “in the wrong place” somehow to me. Having some kind of “more user facing” hook (whether simply a show_term% elaborator or actual metadata) seems useful either way, though.

One way to possibly avoid a core change is modifying the expression (either with metadata if possible, or wrapping it in an application) and introducing a pretty-printer to force it to pretty-print to a plain string in Format (and thus be atomic). This feels like a hack to me, though; we’re exploiting isAtomicFormat in an unintended way.

[Thomas Murrills]

Kyle Miller said:

It would be neat if you could see the elaborated expressions for larger terms somehow.

In this vein, I was also thinking it might be nice to see the elaborated expressions for _’s on hover as well!

[Kyle Miller]

Is this something that needs a flag in the terminfo? Or could this be on the UI side, where maybe there be a key you hold (like shift) that when you hover it shows the term?

[Thomas Murrills]

I think technically this feature would need a flag, since it would be nice to have a way to say "show the term on hover by default (i.e. without needing to press shift)" even if holding shift showed the term.

[Kyle Miller]

Ok, I see, you want an interface to programmatically set what you see when you hover over code. And for this, for your use case, it's enough to override the built-in logic for whether to pretty print the term.

[Thomas Murrills]

Hmm, I guess that's one way of looking at it...but when elaborating syntax to terms, you still do want to consider this to be term info, not merely an arbitrary hover. The thing is that currently a heuristic is used to determine whether to show the underlying term on something, and I'm saying it would be nice to specifically be able to override that heuristic. I feel like displaying terms in hover is a specific task, and simply providing an arbitrary hover whenever we needed to override the heuristic would be "too general".

[Thomas Murrills]

And moreover I imagine that being able to arbitrarily set the hover would, while useful in some circumstances, be quite a big change! This would be a relatively small change.

[Kyle Miller]

(Note that I didn't say anything about arbitrarily setting the hover -- but whatever the case, you're wanting to programmatically control what you see when you hover. That's to say why my suggestion to let it just be a UI issue is not enough for your intended use case.)

[Thomas Murrills]

Ah, I misinterpreted "programmatically" as meaning essentially "by an arbitrary program", sorry.

[Thomas Murrills]

So, in that case, yes! Your interpretation of what I want is correct. :)

[Mario Carneiro]

Thomas Murrills said:

Kyle Miller said:

It would be neat if you could see the elaborated expressions for larger terms somehow.

In this vein, I was also thinking it might be nice to see the elaborated expressions for _’s on hover as well!

I definitely want this

[Thomas Murrills]

Is this enough support to start an RFC on the lean4 repo? (Simply in the interest of not letting things languish, I'll assume it is and start one soon by default—but if anyone would like to tell me otherwise before I do, I'll refrain from doing so.) :)