Tactics are now available in the API docs

Stream: general

[Anne Baanen]

I'm happy to announce that doc-gen4 now also shows tactic documentation! This means if you go to the tactics page in the Mathlib API docs, you will see a list of all the tactics available when you write import Mathlib. For other projects, this page will be generated after you update your doc-gen4 version to the latest commit on the main branch (for users of docgen-action, this happens automatically when you upgrade to the next Lean version).

[Kevin Buzzard]

I went to https://leanprover-community.github.io/mathlib4_docs/tactics.html, found abel, and it says "[abel](https://leanprover-community.github.io/Mathlib/Tactic/Abel.html#Mathlib.Tactic.Abel.abel) and its variants work as both tactics and conv tactics." but the link on abel doesn't work. I tried several other links and they didn't seem to work either.

[Henrik Böving]

I think it's because https://github.com/leanprover/doc-gen4/blob/b2a9fb785e848da488a85989c40512b01fb691c3/DocGen4/Output.lean#L123 needs to be run in a different configuration than the module itself because the link will be served from a different base URL.

[Anne Baanen]

You're right, the issue is that the baseConfig is replaced to generate module docs but it's not correct for other pages. I'll make a PR fixing this in a moment.

[Anne Baanen]

Fixed in doc-gen4#355 (tested to produce the right links on my machine).

[Violeta Hernández]

The formatting seems a bit wonky to me? It'd be nice if each tactic appeared in its own block, like theorems do. Of course, this is a really minor remark, I'm glad we finally have this functionality!

[Jovan Gerbscheid]

I see there is also a "foundational types" section, mentioning Sort u, Type u, Prop, and Pi types. I think that's nice, but maybe it could be expanded to "foundational expressions", so that there can be an item about lambda/fun expressions.

I also notice that at the bottom of this page it mentionsfun α β, α → β (without having explained what fun means), but this should be fun α β ↦ α → β.

[Eric Wieser]

That foundational types page has been there forever

[Eric Wieser]

In particular, the

Note that despite not itself being a function, (→)is available as infix notation for fun α β, α → β.

you refer to is only true in Lean 3

[Eric Wieser]

The purpose of those headings was mainly to collect instances; though it looks like the Pi heading is failing at that

[Chris Henson]

Violeta Hernández said:

The formatting seems a bit wonky to me? It'd be nice if each tactic appeared in its own block, like theorems do. Of course, this is a really minor remark, I'm glad we finally have this functionality!

I agree, something similar to the existing CSS is easier to read, like this:
image.png

Here I also hid tags when empty and moved the module link to a single line.

(and to express the same sentiment as above I think this is wonderful to have, thank you for working on this!)

[Jakub Nowak]

Would it be possible to also have a list of conv-mode tactics?

[Niels Voss]

I don't see some tactics like abel, aesop, ring, use, or order in this list (though I do see aesop_unfold). Is this intentional?

[Chris Henson]

They are usually there, the last docs build had an issue that is being resolved in docgen.