Tactic Index?

Stream: new members

[James Pollard]

Hi all!

For a while I have wanted to have a go at formalising some basic undergraduate maths for fun (e.g. walk through Baby Rudin and Dummit & Foote and try to formalise each proof/exercise); my background is in CS, and I worked quite a lot with Coq in a past life for formalisation of programming language semantic, but it seems that Lean is much more widely used in the mathematics community, so I thought I'd give it a go.

I've been working through Mathematics in Lean to get my hands dirty, and while things are mostly as expected coming from Coq, what I find I'm missing most is the Tactic Index, and I was wondering whether Lean has any equivalent.

It seems there is such a page for Mathlib3, but I can't find a Lean4 equivalent, other than #help tactic, which is slightly hard to read and navigate.

I notice a few comments around the code-base referring to add_tactic_doc, which hasn't been ported from Mathlib3. Is this a pre-requisite for building an index, or could the mechanism behind #help tactic be used?

[Julian Berman]

Does https://seasawher.github.io/mathlib4-help/tactics/ look like what you're after?

[James Pollard]

Julian Berman said:

Does https://seasawher.github.io/mathlib4-help/tactics/ look like what you're after?

Yes! Thanks for the speedy reply :)

Might it be worth adding a link to this somewhere on leanprover-community? Or could there be an "official" hosted version of this (perhaps built and published in Mathlib4 CI)?

[Julian Berman]

There are some old threads discussing that, I don't know what their conclusion is/was.

[Julian Berman]

A quick search says https://github.com/leanprover/lean4/pull/4490 is merged -- I think if my vague memory is right that perhaps the plan is to use that downstream as well.

[Julian Berman]

I can't find where this was discussed last. But I'm sure @Henrik Böving has an opinion or else knows where this was discussed perhaps?

[Henrik Böving]

Yes, the PR was made on request of Robert Lewis (as you can see from the comments) as he wanted to work on infrastructure towards this, I don't know what ended up becoming of that though

[Julian Berman]

(Here's one such "last place" just for cross reference -- https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/.E2.9C.94.20Lean4.20Documentation.20for.20tactics/near/460060777 )

[Joseph Myers]

I've mentioned this a couple of times in the discussions of the new Lean reference manual, since that has documentation for lots of core Lean tactics (not all of them) that would be natural to integrate with documentation for mathlib tactics.