Open utensil opened 4 years ago
I would be very happy to see more structure put into the tactic docs. As of a year ago, mathlib had no documentation standards at all; tactic doc strings, if they existed at all, were purely by the generosity of the tactic writer. The current status is much better, but obviously there's a long way to go.
People are generally willing to contribute documentation. But there's obviously a balance: the more you ask for, the slower it will happen.
What I would suggest is writing a markdown template like yours above, with a few (say, 4-5) headers, and a few suggestions under each of those. Something like
# Summary
* What does the tactic do?
* What scope of problem does the tactic solve?
# Details
* What paramaters can I pass the tactic?
* Are there variants?
# Examples
* Examples that show off all parameter options and variants
# Further notes
* Companion tactics
* Style
* ...
While your list contains a lot of important information, it's a lot, and not every tactic has an answer to every question. I would rather ask for the essential core and get consistent results than ask for the world and get messier results at a slower pace.
As for tags: I'm happy to accept pull requests that change the tag assignments themselves and the html display.
Sorting is complicated. I think it's very important that the docs are generated from the library and not maintained separately. It's hard enough keeping things up to date as it is; there's a reason we moved from a manually "curated" list of tactics to the generation scheme. Of course, this makes it difficult to sort, because sorting isn't a local thing.
As discussed in Zulip, we could:
Provide usage examples for each tactic
Address more aspects of a tactic
ac_refl
,cc
,abel
etc., one stronger than the other)simp
tosqueeze_simp
,simp_only
,rw
etc.)Improve the organization of tags
There're 3 major issues of tags:
conv
,category theory
,equiv
,hypothesis management
,monotonicity
,transport
etc. and not necessarily exhaustive