RFC: Allow doc comments in standalone deriving

Proposal

Standalone derivings

deriving instance I for T

should allow writing a docstring to tag them. So the following spelling is correct

/-- deriving handlers are cool-/
deriving instance I for T

In the case of multiple docstrings like

/-- docs -/
deriving instance I for T1,T2

I propose erroring with a suggestion to split it into 2 statements rather than adding multiple docstrings in a chain above, which seems unnecessary complexity to take on rather than just having the user rewrite it. I don't think giving each one the same docstring makes sense.

The example that led me to this:

deriving instance Hashable for Syntax -- couldn't put docstring here
/-- Make `Syntax` hashable for `matchOnTree` to put in `HashSet` later-/
instance : Hashable Syntax where
  hash syn := Hashable.hash syn

• User Experience: How does this feature improve the user experience?

Users (and machines) benefit from docs, and it makes sense to allow it since it's possible to write a manual doc comment on an instance that calls the derived one (like above).

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?

Moderately advanced ones who'd use this feature and beginners who'd read the docstrings.

• Maintainability: Will this change streamline code maintenance or simplify its structure?

No idea honestly. One question I'm curious about is how this interacts with @[include_doc](I think that's the name).

Community Feedback

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/allow.20adding.20doctring.20to.20standalone.20deriving

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by examining how standalone deriving declarations and doc comments are parsed and associated. The issue mentions no source files or tests; done means supporting a docstring before one standalone deriving declaration and producing a suggestion when one docstring precedes multiple targets.