Term Macro Docstrings

Stream: lean4

[Mac]

A simple term macro gives the docstring of the expanded term rather than the macro:

/-- Docstring for `dummyFoo` -/
constant dummyFoo : Unit

/-- Docstring for `__foo__` -/
macro stx:"__foo__" : term => return Lean.mkCIdentFrom stx ``dummyFoo

#check __foo__ -- Hover gives the docstring for `dummyFoo` rather than `__foo__`

Is there any way to get it to give the macro's docstring instead?

[Sebastian Ullrich]

That's an interesting edge case. Since the pretty printer does show dummyFoo : Unit in any case (but maybe that's not desirable either), I think showing its docstring is defensible, but we could then append the elaborator's docstring as well. What do you think?

[Mac]

Sebastian Ullrich said:

That's an interesting edge case. Since the pretty printer does show dummyFoo : Unit in any case (but maybe that's not desirable either), I think showing its docstring is defensible, but we could then append the elaborator's docstring as well. What do you think?

In my case I would very much like show just the macro at both the pretty print and docstring level. But, any improvement would be nice.

[Sebastian Ullrich]

I don't know what the appropriate default behavior should be in general, but ‹_› comes to mind for a macro where printing the resolved identifier seems desirable

[Mac]

Sebastian Ullrich said:

I don't know what the appropriate default behavior should be in general, but ‹_› comes to mind for a macro where printing the resolved identifier seems desirable

I think that is a fine default. I would just like a way to change that behavior when appropriate. Also, my specific use case in a macro-like elaborator, rather than a pure macro., so I have more power to do whatever is necessary.

[Mac]

My current workaround is to put the macro docstring on the constant and give the constant the same name, but it is rather inelegant (and will look very back in the generated docs).

[Sebastian Ullrich]

Mac said:

Sebastian Ullrich said:

I don't know what the appropriate default behavior should be in general, but ‹_› comes to mind for a macro where printing the resolved identifier seems desirable

I think that is a fine default. I would just like a way to change that behavior when appropriate. Also, my specific use case in a macro-like elaborator, rather than a pure macro., so I have more power to do whatever is necessary.

In that case, wrap your term in an id application or something :)

[Mac]

Sebastian Ullrich said:

In that case, wrap your term in an id application or something :)

That works rather well, neat! Thanks a bunch! Also, I notice keywords of the form __blah__ don't get the keyword syntax highlighting, why?