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!

[Asei Inoue]

@Haruhisa Enomoto

Thank you for making your tactic list.

I created a GitHub Action to automatically update tactic list following your way.
https://github.com/Seasawher/mathlib4-tactics/tree/main

[Bolton Bailey]

It would be very cool if this could be integrated with https://leanprover-community.github.io/ for increased accessibility

[Asei Inoue]

I have made web page to see mathlilb4 tactics.

https://seasawher.github.io/mathlib4-tactics/

[Asei Inoue]

It would be very cool if this could be integrated with https://leanprover-community.github.io/ for increased accessibility

Should I open a PR?

[Damiano Testa]

Would it be possible to have each tactic be its own section and have them appear in a table of contents on the left?

Maybe just prefixing each "syntax" by # would be enough?

[Mario Carneiro]

mdbook only uses the sidebar for separate pages AFAIK

[Damiano Testa]

Ah, that's too bad, separate pages would not be especially good, I think.

[Asei Inoue]

Would it be possible to have each tactic be its own section and have them appear in a table of contents on the left?

It is possible to display a table of contents within a page.

[Asei Inoue]

By the way, there is a lot of code that is lean code but is simply enclosed in "\```" instead of "\```lean".
It may be useful to have a linter that warns against code blocks enclosed in mere "```".

[Mario Carneiro]

I think it's safe to say that the default language used in lean doc comments is lean. So if you are presenting markdown from lean doc comments elsewhere, you should either set the default language if possible, or fix this with some regex

[Asei Inoue]

you should either set the default language if possible, or fix this with some regex

ok I will use regex.

[Asei Inoue]

I can make a similar list by #help command outputs.
Someone want this?

[Kevin Buzzard]

I don't think it's unreasonable to suggest that anything not in the API docs will be wanted by somebody.

[Kevin Buzzard]

Furthermore, having "unofficial" solutions to these sorts of problems is a good way of getting the community to think a bit harder about solutions hosted on the community website or API docs.