Adding docstrings from within attributes after lean4#10307

Stream: lean4

[Thomas Murrills]

lean4#10307 restricts the previously monad-polymorphic API for adding docstrings, which worked in AttrM, to TermElabM. This causes issues for attributes like @[to_additive /-- example docstring -/], which allow specifying docstrings for generated declarations, and need a way to attach them to declarations within abbrev AttrM := CoreM.

How should docstrings be added to generated declarations from within attributes? To put some possibilities out there, I can think of three ways, depending on the details of verso docstring parsing/elaboration and future plans:

1. Make addMarkdownDocString monad-polymorphic such that it works in CoreM. However, this runs the risk of adding verso-styled docstrings as markdown docstrings incorrectly; so, is there a quick way to check if a docstring is intended to be "verso-style" (i.e. without actually elaborating it)? If so, some version of addMarkdownDocString could log an error on verso-style docComments. (But this is only relevant if addMarkdownDocString will be staying around.)
2. Just runTermElabM in CoreM to elaborate the docstring. But when is it safe to do this? What parts of the ambient TermElabM state might verso docstrings depend on, and when might its absence cause unexpected behavior?
3. A more complex change: allow attributes to optionally access the TermElabM state. This would require some thought, but could mean equipping AttrM with a readable value of e.g. type Option Term.State (etc.) which would be passed when called from a high enough monad (and, maybe, only if the attribute opted-in to receiving it via some flag). Not sure if this would be a problem for performance or parallelism somehow, though. (I'm only suggesting this because I can imagine it being more generally useful; other attributes might want to process their syntax in TermElabM too.)

[David Thrane Christiansen]

Thanks for checking!

I'll see what I can do to make this work polymorphically again, and failing that, provide an AttrM wrapper that makes sure the state is set up as it should be.

The way to check if a docstring should be Verso is to check the value of the option doc.verso. You should take a bit of care - when docstrings are processed separately (e.g. delayed by some other process), the value of the option should be saved with them, so that it's truly the value at the time the docstring is encountered that is used.

[David Thrane Christiansen]

https://github.com/leanprover/lean4/pull/10357 makes the Markdown docstring API monad-polymorphic again. It's not the right long-term solution, but it will fix the short-term adaptation hassle.

[Thomas Murrills]

David Thrane Christiansen said:

The way to check if a docstring should be Verso is to check the value of the option doc.verso.

Ah, I think I see; so the responsibility is with the docstring writer to ensure doc.verso is true when they want to use verso syntax, right?

Do you think there's an easy way to tell if a docstring "would be fine" if included as a markdown docstring even when doc.verso is true (i.e. to easily detect that it has no special verso syntax)? (Or should we not take that approach anyway, for other reasons, e.g. a docstring is unlikely to work as both markdown and verso/etc.?)