Mathlib4 tactics list?

Stream: mathlib4

[Haruhisa Enomoto]

In mathlib3, there's an official list of tactics: https://leanprover-community.github.io/mathlib_docs/tactics.html
I learned a lot from it, but I cannot find the mathlib4 version. Is it scheduled for release? Or are there any ways to find all the tactics?

[Jireh Loreaux]

It's not ideal, but you can use #help tactic my_tactic to get information about my_tactic. If you don't provide a tactic, then it lists all of them, but the list is a bit unwieldy.

[Asei Inoue]

Can we use Lean to automatically convert the #help tactic output to markdown and save it?

[Alex J. Best]

You could (if you right click on #help tactic or #help cat tactic and jump to definition, you can see how it is implemented which you could repurpose). But in this case seeing as everything is already indented properly its probably simpler to copy-paste the output and use other tools to process it into the format you want.

[Haruhisa Enomoto]

Thank you all for letting me know #help tactic!
I manually formatted it into markdown and made it available at:
https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md

[Kevin Buzzard]

I claim that this file is now the canonical way to look up tactic documentation on mobile, which is strong evidence that doc-gen is missing a trick. Thank you Haruhisa!