doc: write a guideline for tactic docstrings #11406
Conversation
At the Mathlib Initiative we want to ensure that tactics have good documentation. Since this will involve adding documentation to tactics built into core Lean, I discussed with David that we should have a shared set of documentation guidelines that allow me to do my work both on the Lean and on the Mathlib repositories. I have already shown an earlier version of this guideline to David who made some helpful suggestions but would be away. So to make sure the discussion doesn't get lost, I've made a PR with the version I ended up with after the first round of comments.
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
Reference manual CI status:
|
doc/style.md
Outdated
|
|
||
| The **short summary** should be 1–3 sentences (ideally 1) and provide | ||
| enough information for most readers to quickly decide whether the | ||
| docstring is relevant to their task. The first (or only) sentence of |
There was a problem hiding this comment.
How about:
| docstring is relevant to their task. The first (or only) sentence of | |
| tactic is relevant to their task. The first (or only) sentence of |
There was a problem hiding this comment.
I adapted this sentence from the section about constants, so I'll make the same change there. (Feel free to revert.)
doc/style.md
Outdated
| is an example invocation of the tactic, written in present tense | ||
| indicative. If the example tactic invocation names parameters, then the | ||
| short summary may refer to them. The summary should be written as a | ||
| single paragraph. |
There was a problem hiding this comment.
What do we do here if the tactic invocation is somewhat syntactically complicated, like match? We should have consistent conventions here. Would we want match e with alts..., for instance, with a second sentence "Each of the alts... has the form | pat (| pat)... => tactics"?
There was a problem hiding this comment.
Existing tactic docs take a lot of different approaches here. For the introduction I'd like to encourage brevity, we don't want to take up all the space with describing the syntax before we can get to the use. So my preference is to take a representative example over completeness: rw [e], not rw [e1, e2, ...]. This is already what we do for cases and induction: "induction x applies induction on x to the main goal, producing one goal for each constructor [...]" and later describing with using an example. (Although I'm not too fond of the docstring, since the bulleted list of syntax forms lists both general explanations and specific examples.)
How does something like this sound?
For the example invocation, prefer the simplest representative example. Explain more complicated forms in the variants section. If needed, abbreviate the invocation by naming part of the syntax and expanding it in the next sentence.
| explanatory examples that can’t necessarily be machine checked and | ||
| don’t fit the format. | ||
|
|
||
| **Variants**, if needed, should be a bulleted list describing different |
There was a problem hiding this comment.
It seems to me that some tactics may have large variants. How would the docs for induction look in this format? Perhaps the variants should also be able to have names? In Verso, we have a construct like HTML <dl> or LaTeX description that's great for this, and Markdown could have a convention of sticking a title in bold after a bullet.
Perhaps the restriction on having the example as the subject of the sentence can be one option, and a short summary of the syntactic difference be another?
Like:
* **Named cases***
A `with` clause results in the cases generated by the tactic being invoked by name, with the tactic ensuring that all cases are handled. `induction e with (pre:tacticSeq)? ((| lbl:ident var:ident*)+ => tacticSeq)+` first runs `pre` in each subgoal, after which the cases labels of all subgoals not closed by `pre` are matched to the provided tactics.
(that text isn't the best, but I think it illustrates a reasonable format that's a bit more accessible than sticking the tactic first).
There was a problem hiding this comment.
I'm a big fan of <dl>! How does the following sound:
Each list item should describe an individual variant
and take one of two formats: the short summary as above, or a
named list item. A named list item consists of a title in bold
followed by an indented short paragraph.
| should be clear whether the tactic fails if it does not close the main | ||
| goal and if it creates any side goals. The details may include | ||
| explanatory examples that can’t necessarily be machine checked and | ||
| don’t fit the format. |
There was a problem hiding this comment.
Should intentional extension points also fit in here? I'm thinking of tactics that are intended to be extended either by giving them additional macro_rules or by giving some helper tactic the macro_rules. Or should they have a separate paragraph?
There was a problem hiding this comment.
Agreed, we should mention extensibility in/next to the details section.
For macro_rules based extensible tactics, a paragraph plus example seems the currently standard form, and I think that's sufficient. For example:
You can use the command
macro_rulesto extend the set of tactics used. Example:macro_rules | `(tactic| trivial) => `(tactic| simp)
For tactics like ext or grw that use attributes, most explanation should live with the attributes. A single sentence mentioning the attribute here is good though, because it's not obvious that grw looks for @[gcongr] or @[mono] attributes.
Proposal:
If the tactic is extensible using
macro_rules, mention this in the
details and give a one-line example. If the tactic provides an attribute
or a command that allows the user to extend its behavior, the
documentation on how to extend the tactic belongs to that attribute or
command. In the tactic docstring, use a single sentence to refer the
reader to this further documentation.
There was a problem hiding this comment.
This absolutely makes sense to me and I think it's fine as is. However, I would note that as someone who hasn't done as much proving myself, I'm not familiar with macro_rules extension at all and would find your proposed example text a bit confusing! It might be worth describing * Macro Extension as an optional part of the description between * Details and * Variants, and maybe giving (or pointing to) some examples of good tactic documentation that includes macro expansion documentation.
| keyword) that invokes the tactic. When the effect of the tactic is not | ||
| clear from the code, you can use code comments to describe this. |
There was a problem hiding this comment.
| keyword) that invokes the tactic. When the effect of the tactic is not | |
| clear from the code, you can use code comments to describe this. | |
| keyword) that invokes the tactic. When the effect of the tactic is not | |
| clear from the code, you can use code comments to describe this. Do | |
| not include text between examples, because it can be unclear whether | |
| the text refers to the code before or after the example. |
If this is the intent, I think it's worth documenting it.
5 participants
This PR covers tactic docstrings in the documentation style guide.
At the Mathlib Initiative we want to ensure that tactics have good documentation. Since this will involve adding documentation to tactics built into core Lean, I discussed with David that we should write a shared set of documentation guidelines that allow me to do my work both on the Lean and on the Mathlib repositories.
I have already shown an earlier version of this guideline to David who made some helpful suggestions but would be away for a few days. So to make sure the discussion doesn't get lost, I've made a PR with the version I ended up with after the first round of comments.