documenting attributes

Stream: mathlib4

[Kevin Buzzard]

I'm trying to review a PR which has an @[reassoc] in, and if I hover over it I get the useless Syntax for the `reassoc` attribute. I can figure out what @[reassoc] does by adding whatsnew in and then seeing what the attribute did, and I've just done this, so at this point I know what reassoc does. Within a week I will have forgotten again. Can I change this "Syntax for..." message to an explanation of what @[reassoc] does, or should this information go elsewhere?

I had this issue with another attribute the other day, but I've forgotten which attribute it was; once I understand what I'm allowed to do here I'll document other attributes as I come across them.

[Damiano Testa]

I suspect that what you are seeing is the doc-string for docs#CategoryTheory.reassoc, so maybe editing that doc-string will help!

[Damiano Testa]

For a lot of the declarations in Mathlib.Tactic I find that it would be very useful to make the module-docs also be the doc-string for the "main" declaration. I wonder if we could have an attribute @[inherit_doc "module-docs"] that would allow that.

[Damiano Testa]

Or some polished version of this:

import Lean.Elab.Command
import Lean.Elab.DeclarationRange

import Mathlib.Tactic.CategoryTheory.Reassoc

open Lean Elab Command in
-- copy-pasted from `Lean.Elab.Command.elabAddDeclDoc`
elab "add_docs " mod:ident &"to" id:ident : command => do
  let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
  unless ((← getEnv).getModuleIdxFor? declName).isNone do
    throwError "invalid 'add_module_doc', declaration is in an imported module"
  let dc := getModuleDoc? (← getEnv) mod.getId
  let docs := dc.getD #[]
  if h : docs.size = 0 then
    throwError "No doc-module strings in {mod}!"
  else
  if let .none ← findDeclarationRangesCore? declName then
    -- this is only relevant for declarations added without a declaration range
    -- in particular `Quot.mk` et al which are added by `init_quot`
    addAuxDeclarationRanges declName (← getRef) id
  addDocString declName (docs[0].doc.dropWhile (· != '\n'))

-- hover, no docs
theorem hello : True := .intro

add_docs Mathlib.Tactic.CategoryTheory.Reassoc to hello

-- hover to see the `Mathlib.Tactic.CategoryTheory.Reassoc` module doc-string!
#check hello

[Kim Morrison]

I like the idea of an @[inherit_module_doc] attribute.

[Damiano Testa]

Ok, I've found myself wanting it a few times. I think that by being a little structured about how the "header" of the module docs looks like, the attribute can be relatively straightforward.

[Kyle Miller]

For some extra context, Kevin added a docstring to reassoc at #14447

[Kyle Miller]

I'm not sure about inherit_module_doc... I feel like a lot of module docstrings are not good tactic documentation. At least the ones I write explain some of the implementation.

[Kyle Miller]

I wouldn't want people to write module docstrings that are sub-par just to make them be good tactic docstrings, and vice versa.

[Damiano Testa]

If the implementation is in a "second" module doc, this could work, though.

[Damiano Testa]

Anyway, I often find that I mention in the module docs to look at the tactic doc for more details, in order to avoid having to keep in sync the information.

[Damiano Testa]

But to be fair, I also thought that extend_docs was very useful and honestly it is very niche!

[Thomas Murrills]

It would be nice to be able to reuse text somehow to avoid copy-pasting as much as possible! One idea is to allow inheriting specific markdown sections as the docstring; e.g. given

/-! # The `foo` tactic

## Description

`foo` fooifies the goal state.

## Implementation

This tactic is implemented in an extremely complicated way.
The story begins in 1800 B.C., when the first known fooification algorithm
was inscribed onto a clay tablet in cuneiform...
-/

you could write something like @[inherit_module_doc (section := ##Description)].

[Damiano Testa]

I think that if you segment the doc-module, then you can use the segment that you want:

/-!
Segment 1
-/
/-!
Segment 2
-/
...

Then you could make inherit_module_doc take a numeral input.

[Thomas Murrills]

(In general it would be nice to be able to declare "blurbs" which could be interpolated easily into docstrings, which is a task in service of the same goal, but is much more difficult to implement.)

[Thomas Murrills]

Damiano Testa said:

I think that if you segment the doc-module, then you can use the segment that you want:

/-!
Segment 1
-/
/-!
Segment 2
-/
...

Then you could make inherit_module_doc take a numeral input.

I'd worry this would be a little fragile and awkward-looking in source; also doing something like section := ##Description is more reflective of purpose than referring to a numerical index! :)