Custom tooltips from macros

Stream: lean4

[David Thrane Christiansen]

In Racket, it's convenient to have macros that associate custom tooltips with bits of syntax during expansion. This is used e.g. in Typed Racket to show the types of expressions, and for various embedded languages to report information back to users. Is there a way to do something like this in Lean 4? I could imagine exposing the information through the LSP "hover" method, for instance.

[Leonardo de Moura]

Could you please elaborate on the potential use cases? We already have hover with type information in our LSP server.
image.png
How would the user-provided ones interact with the existing hover information?

[David Thrane Christiansen]

Let's say I wrote a macro to generate an LALR parser automaton from a description of the grammar (Racket's is described here: https://docs.racket-lang.org/parser-tools/LALR_1__Parsers.html#%28form._%28%28lib._parser-tools%2Fyacc..rkt%29._parser%29%29 ). It would be convenient for users to get hover information that describes things like shift-reduce conflicts, the relationship between a given operator precedence and the others in the grammar, and the like.

Similarly, let's say I'm porting Software Foundations and I use a macro to embed a nice syntax for one of the object languages being studied. This macro type checks the embedded terms using the object language type system. It would be nice to add hover info with those types.

Finally, I might want to write a client for a system with an OpenAPI spec. It would be useful to add hover information to HTTP request paths based on an IO call that my macro did. This is the "type providers" use case.

[David Thrane Christiansen]

As far as how to interact, I'm not totally sure. One possibility is to add it and show both. Another is to replace the built in version. I'm imagining an API in an elaboration monad m that is something like:

addHover : Syntax -> HoverDoc -> m Unit

Where HoverDoc is a datatype describing things like paragraphs, type signatures, and strings.

[David Thrane Christiansen]

And the Syntax is expected to be the original syntax object from the user's program

[Wojciech Nawrocki]

A seedling of an API like this already exists. It is not currently in use as we ended up not having a need for it, and as far as I remember it is not hooked up to anything in the LSP server so is not actually accessible from the editor. We might also prefer custom data in Info rather than in InfoTree directly. But what you are describing sounds like it would need such a capability to store "user data" as part of elaboration output. I think a method addHover : HoverDoc → m Unit would suffice since monads in the elaborator stack implement MonadRef. Probably the existing functionality closest to what you want is logInfo, but of course that will result in lots of squiggles in the editor whereas an on-hover info would be hidden by default.

[Leonardo de Moura]

@David Thrane Christiansen

It would be convenient for users to get hover information that describes things like shift-reduce conflicts

You can use the existing errors/warnings APIs for this.

the relationship between a given operator precedence and the others in the grammar, and the like.

This can be useful.

Similarly, let's say I'm porting Software Foundations and I use a macro to embed a nice syntax for one of the object languages being studied.

I think this one is artificial. First, they don't write many programs in the object languages they study. The types in the object language often depend on a context that is not available when processing the macro. To support this correctly, I think one has to write their own elaborator for the object language. I can see scenarios where this may happen: one is implementing their own embedded DSL like @Mac's Alloy https://github.com/tydeu/lean4-alloy/blob/master/examples/my_add.lean

Finally, I might want to write a client for a system with an OpenAPI spec. It would be useful to add hover information to HTTP request paths based on an IO call that my macro did. This is the "type providers" use case.

This one is also useful.

[Leonardo de Moura]

Wojciech Nawrocki said:

A seedling of an API like this already exists. It is not currently in use as we ended up not having a need for it, and as far as I remember it is not hooked up to anything in the LSP server so is not actually accessible from the editor. We might also prefer custom data in Info rather than in InfoTree directly. But what you are describing sounds like it would need such a capability to store "user data" as part of elaboration output. I think a method addHover : HoverDoc → m Unit would suffice since monads in the elaborator stack implement MonadRef. Probably the existing functionality closest to what you want is logInfo, but of course that will result in lots of squiggles in the editor whereas an on-hover info would be hidden by default.

I agree.

[Sebastian Ullrich]

@Leonardo de Moura There is also some overlap with the idea of attaching more helpful information to syntax consumed by elaborators of other syntax, e.g. \cdot, that we recently discussed. For \cdot specifically, we could reuse the current TermInfo to attach the type as well as elabBadCDot as a "faux" elaborator that we can write a docstring for. However, what wasn't immediately clear to me is when and how to insert this information into the info tree such that it is still well-formed, since so far we did not have to worry about possibly-overlapping subtrees in the info tree.