feat(tactic): command for adding tactic, command, and attribute documentation (RFC)

[robertylewis]

As discussed in #1874, the current setup of tactics.md, etc isn't ideal. The entries often repeat information found in doc strings; they're located far from the definitions, so it's easy to forget to update them; the doc generator does something hackish to parse individual entries out of the markdown file.

This PR introduces a command add_tactic_doc that registers a "documentation entry" related to a declaration/list of declarations. It's best displayed by invoking it on itself:

add_tactic_doc
{ name := "add_tactic_doc",
  category := doc_category.cmd,
  decl_names := [`add_tactic_doc_command],
  tags := ["documentation"],
  description :=
"A command used to add documentation for a tactic, command, hole command, or attribute.

Usage: after defining an interactive tactic, command, or attribute, add its documentation as follows.
```
add_tactic_doc
{ name := \"display name of the tactic\",
  category := cat,
  decl_names := [`dcl_1, dcl_2],
  tags := [\"tag_1\", \"tag_2\"],
  description := Ädescribe what the command does here\"
}
```

The argument to `add_tactic_doc` is a structure of type `tactic_doc_entry`.
* `name` refers to the display name of the tactic; it is used as the header of the doc entry.
* `cat` refers to the category of doc entry.
  Options: `doc_category.tactic`, `doc_category.cmd`, `doc_category.hole_cmd`, `doc_category.attr`
* `decl_names` is a list of the declarations associated with this doc. For instance,
  the entry for `linarith` would set ``decl_names := [`tactic.interactive.linarith]``.
  Some entries may cover multiple declarations.
  It is only necessary to list the interactive versions of tactics.
* `tags` is an optional list of strings used to categorize entries.
* `description` is the body of the entry.
  What you are reading now is the description of `add_tactic_doc`.

If only one related declaration is listed in `decl_names` and it does not have a doc string,
`description` will be automatically added as its doc string.

Note that providing a badly formed `tactic_doc_entry` to the command can result in strange error messages.
"  }

Happy to hear any suggestions about this!

I haven't ported the entries from tactics.md yet. I'd rather get feedback first, merge this, and do that in a separate PR. Of course, the doc generation tool has to be updated too before deleting the .md files.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[robertylewis]

There are a few annoyances:

• Writing a doc entry is a little more annoying than editing the .md, since you have to do it in a Lean string (with escaped quotation marks) and without the aid of editor .md support.
• There's a weird error when you give the command a malformed structure: vm check failed: is_closure(o) (possibly due to incorrect axioms, or sorry). This is some kind of bad parser/tactic interaction but I couldn't figure out how to provide a better error.

[jcommelin]

Would it be possible to write it as docstring first, to get editor support. And then hit a button to convert it to a Lean string. Maybe to complicated...

[robertylewis]

I suppose it could be set up to "inherit" the description from the doc string of an existing declaration, in roughly the same way that the description can become the doc string. I think editor support for escaping quotations in a string sounds a little clunky. Plus, you still don't get real markdown support in a comment like you do when you're editing an actual markdown file.

[robertylewis]

Regarding the annoyance of writing markdown blocks inside of Lean strings: only five entries in tactics.md use quotation marks, although there are more in commands.md and hole_commands.md. I can imagine this would get frustrating eventually. It would also be hard to preview entries.

One hackish alternative is, instead of using a command, actually defining objects. So your doc entry would look like

/-- A tactic for doing this and that. This is the markdown content. -/
meta def doc_info.my_tac : tactic_doc_entry :=
{ name := ...,
  ... }

This looks ugly and it forces you to name the entry (in a way that won't ever be used). So I don't like it much.

Another option would be to force the entry to be inherited from the doc string for a tactic.

/-- This is the doc string for linarith. It's also the linarith entry in tactics.md -/
meta def tactic.interactive.linarith : ...

add_tactic_doc {
  name := "linarith",
  decl_name := `tactic.interactive.linarith,
  ... } -- no description field

But I think forcing doc page entries and doc strings to be the same is a bad idea. It also complicates the picture a bit for tactic "families" like finish/clarify/safe (this is why decl_names is currently a list).

A third, related, option would be to do option 2, but with a delimiter in the doc string. You write the standard doc string, a bar ----------, and then the tactic doc entry. add_tactic_doc will split the string at the delimiter, replace the doc string with just the top part, and use the bottom part as the doc page entry. This is also hackish and needs a change in C++ since you currently can't overwrite doc strings. It doesn't help the situation with tactic families.

A fourth, nuclear, option is changing the parser to make this easier.

[gebner]

A third, related, option would be to do option 2, but with a delimiter in the doc string. You write the standard doc string, a bar ----------, and then the tactic doc entry. add_tactic_doc will split the string at the delimiter,

We can also keep the docstring as it is and only split it for the documentation. vscode doesn't have a problem with the long docstring, it only shows the beginning if it's too long (you need to scroll to see all of it).

[bryangingechen]

Would it be possible to have an option to read markdown strings from standalone markdown files?

e.g. something like:

add_tactic_doc
{ name := "add_tactic_doc",
  category := doc_category.cmd,
  decl_names := [`add_tactic_doc_command],
  tags := ["documentation"],
  description_file := "path/to/some_markdown_file.md" -- instead of description

[robertylewis]

A third, related, option would be to do option 2, but with a delimiter in the doc string. You write the standard doc string, a bar ----------, and then the tactic doc entry. add_tactic_doc will split the string at the delimiter,

We can also keep the docstring as it is and only split it for the documentation. vscode doesn't have a problem with the long docstring, it only shows the beginning if it's too long (you need to scroll to see all of it).

I think this is probably the most practical solution. There are still a few minor hiccups. For one, it doesn't help the "family of tactics" situation, although in practice that's not very common. We'll have to use the same scheme in core to document tactics there, since we can't overwrite their doc strings from mathlib. But this is all manageable.

Would it be possible to have an option to read markdown strings from standalone markdown files?

One of the reasons for this change is so that the declarations and docs aren't so distributed. It would be better than the current situation, but still feels a little messy to me.

[robertylewis]

I tried to implement Gabriel's suggestion earlier today. But a fortunate choice of test case pointed out an issue very quickly: Lean doesn't like nested comment blocks. So a tactic doc entry that contains comments, e.g. the one for library_note, can't be entered as a doc string.

One proposed solution: change the lexer to accept nested comments. @gebner suggested this might be a "medium effort" task. I don't want to do it myself, but maybe someone is interested?

[bryangingechen]

Oh, that's interesting. I believe Lean is actually fine with nested "non-doc" comment blocks, e.g.:

/- this is fine:
  /- nested! 
   /- even more nested
    -/
  -/
-/

so the new feature would be extending this somehow to (module) docstrings.

edit: Oops, Gabriel already said more or less the same thing on Zulip. He also pointed out the key function is read_comment_block)

[bryangingechen]

I can help out with this later tonight if there's still work to be done. Should I work in revisions from my previous PR #1874 or should that go in a different PR?

[robertylewis]

I can help out with this later tonight if there's still work to be done. Should I work in revisions from my previous PR #1874 or should that go in a different PR?

Thank you! I'm done for the night, so everything left is fair game. Feel free to work in your revisions if you want, or in a separate PR, your call. Also feel free to do whatever you want with the tags field. I haven't been very consistent with it so far; it will be easier to clean that up in a second pass, I think.

[bryangingechen]

I think I got the rest of the tactics, commands and hole commands. Along the way I added in most of my tweaks from #1874, added a few module docs, cleaned up some docstrings and split some long lines in the tactic files. Feel free to revert any changes I made if they seem excessive.

A few notes:

• Can we somehow allow tactic doc entries with different categories to share the same name? For instance, there is an attribute, a tactic, and a hole command all named tidy. I labeled the instances like this with comments reading "TODO: name conflict".
• I didn't work too hard on the tags, so a bunch of them are still empty / inconsistent.
• At some point we should also go through and make internal links.
• I tried to remove excess indentation from docstrings since I saw that VS Code was rendering some of the indented lines as code in the markdown.
• It looks like a merge conflict has appeared. I haven't tried to fix it yet since I wasn't confident that I wouldn't screw up the git history somehow, as I imagine we'll have to rebase all this on the 3.6.0 branch again.

[bryangingechen]

A few more thoughts:

• Can we have doc_gen automatically display what imports are necessary for a given tactic / command to work? (e.g. import tactic.basic or import tactic as well as the actual file the tactic is defined in.)
• So far it looks like we've only added tactic doc entries for tactics which are meant to be used in the course of writing a proof. There are also a bunch of tactics which are mainly used for writing new tactics or tests. Perhaps we should make a new category for those?
• We should remember to update /docs/contribute/doc.md
• docs/extras.md is currently out of date (the cc file is gone)

[robertylewis]

Thanks, Bryan! That's fantastic.

• Can we somehow allow tactic doc entries with different categories to share the same name?

For sure, that's easy enough to do.

• It looks like a merge conflict has appeared.

I'll investigate once #2064 lands. I think there's no point fixing it before then.

• Can we have doc_gen automatically display what imports are necessary for a given tactic / command to work? (e.g. import tactic.basic or import tactic as well as the actual file the tactic is defined in.)

Yep, this is the plan. It will use the decl_names field to compute this.

• So far it looks like we've only added tactic doc entries for tactics which are meant to be used in the course of writing a proof. There are also a bunch of tactics which are mainly used for writing new tactics or tests. Perhaps we should make a new category for those?

I think the API docs are really the place to look for this kind of thing, e.g. tactic.core. We should eventually improve the high level tactic writing docs.

[robertylewis]

I just noticed this PR is from a branch on my own repo. I'm going to close it and reopen it from a community branch.