docstring style guide

[PatrickMassot]

Leo asked for help from the community to write docstrings in the Lean 4 codebase. It would be nice to have a docstring style guide to help in this effort and ensure some consistency. Below I'll list some questions but feel free to ignore any item that you think is irrelevant.

Potential questions includes:

• Should docstring refer to variable names? Right now this is confusing since tooltips don't show those names, only the signature, but this will hopefully improve. Mario points out that variable names are user-facing since we can use named argument in function calls.
• How to start the docstring of a function? We don't have to impose a style but if you have preferences then it's better to tell before people start writing. Existing styles include
  • Using a sample function call. For instance the docstring of ReaderT.adapt starts with "adapt (f : ρ' → ρ) precomposes function f"
  • An infinive verb (or is it conjuguated using imperative?) like "Execute an EStateM on initial state s to get a Result." for EStateM.run
  • A conjuguated verb like "Converts a UInt64 to a USize by reducing modulo USize.size." for UInt64.toUSize
• Do we want a rigid way of "repeating the signature" such as the ones for python listed at http://daouzli.com/blog/docstring.html?
• How should we describe possible failures? Some existing docstrings don't mention failure at all. Some say "fails if..." without anything specific, some mention throwing exceptions or panicking.
• Is it ok to have docstring that refer to other declarations in an essential way? For instance the docstring of ReaderT.readThe is "Like read, but with ρ explicit. This is useful if a monad supports MonadReaderOf for multiple different types ρ."

We also need an answer to the syntax vs elab discussion from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.5BRFC.5D.20Hover.20doc.20strings.20.28lean4.231443.29.

On a slightly different topic, I think it would be nice to have some list of files to prioritize since there are so many files to document.

[leodemoura]

@digama0 You made great suggestions during the last dev meeting. It would be great if you could document them here.