Tactic reference

Stream: general

[Richard L Ford]

I'm studying Lean 4, and in the various documents (e.g. Theorem Proving in Lean, Mathematics in Lean, ...) tactics are introduced a bit at a time, which is fine as a tutorial. But I'm wondering if there is any reference list of all the tactics. Also, I believe some tactics are introduced in the base Lean, maybe others in the standard library, yet others from the mathlib. It would be nice to have a reference, with each tactic listed as to its source.

[Patrick Massot]

We had such a list in Lean 3 but restoring it in Lean 4 is on our collective todo list.

[Damiano Testa]

While the list gets implemented, running

#help tactic

lists all tactics in the environment (I don't remember where #help is defined, so some import is necessary).

[Richard L Ford]

Damiano Testa said:

While the list gets implemented, running

#help tactic

lists all tactics in the environment (I don't remember where #help is defined, so some import is necessary).

Thanks. That is very helpful.

[Damiano Testa]

You can also use #help attr, command and probably more things: the doc-string should be quite informative.

[Jireh Loreaux]

And in case it isn't obvious, if you know the name of a tactic, like ring, you can just do #help tactic ring

[Richard L Ford]

I'm wondering where "#help" is documented. I do not see it in the Lean manual or in the Theorem Proving in Lean book.

[Richard Copley]

You can see some documentation for the #help command using the command #help command (:smile:)

[Emilie (Shad Amethyst)]

But can you do #help #help?

[Richard Copley]

First thing I tried!

[Edward van de Meent]

#help command "#help" should do the trick

[Edward van de Meent]

notably, #help command help and #help command #help don't, though

[Julian Berman]

@Richard L Ford if you (also) mean to ask "how should you know #help exists" I think that's a good question and I don't know the answer!

[Julian Berman]

Is there a command which lists all #commands?

[Edward van de Meent]

unhelpfully, that's what #help command does (along with the documentation)

[Julian Berman]

Idly -- that (#help command) doesn't render fully correctly for you I assume right? When I saw it didn't render right in lean.nvim just now I thought I was missing something, but it looks like no, the diagnostic that returns looks like it's markdown, but diagnostics are apparently not supposed to contain markdown according to the spec (at least not until / if https://github.com/Microsoft/language-server-protocol/issues/250 ever gets accepted), and it looks like that doesn't render right in VSCode either from what I see. CC @Marc Huisinga maybe if you don't mind the ping, even though I know that command looks defined in Mathlib, not Std or core?

[Richard L Ford]

My next question is, where is #help implemented? I grepped the lean4 repo and did not find a reference to "#help". Is it implemented by lean4, or some higher layer, like in the language server?

[Julian Berman]

(The language server is inside the lean4 repo) -- It's implemented in Mathlib. You can see where by using goto definition -- specifically if you press F12 or hold down ctrl while you're over #help you'll get taken to Mathlib/Tactic/HelpCmd.lean

[Richard L Ford]

Julian Berman said:

(The language server is inside the lean4 repo) -- It's implemented in Mathlib. You can see where by using goto definition -- specifically if you press F12 or hold down ctrl while you're over #help you'll get taken to Mathlib/Tactic/HelpCmd.lean

Cool. Thanks. Mystery solved. And that explains why it is not mentioned in the Lean manual. However, it seems like a parenthetical comment like "And for users of the mathlib, there is the #help tactic" would be useful in the Lean manual as well as Theorem Proving in Lean, and certainly in the Mathematics in Lean book.

[Julian Berman]

I don't see it mentioned previously from a Zulip search but it seems perhaps like #help could move to Std (which is relevant only inasmuch as it'd change where such a document would point you to. I definitely agree it'd be nice if it were mentioned somewhere).

[Kim Morrison]

#help should move all the way to Lean, I think. Are there any awkward dependencies?

[Kim Morrison]

I can review if someone would like to do it. There is some trickery to make it a built-in commands that works without imports. If you don't want to do that part, just flag it in the PR description and someone can help out.

[Kim Morrison]

@David Thrane Christiansen, does this sound right? We do need an in-lean mechanism to look up all tactics / commands, I think.

[Mario Carneiro]

Scott Morrison said:

#help should move all the way to Lean, I think. Are there any awkward dependencies?

No, and I support this move

[Mario Carneiro]

The output could use some work though. I did the best I could under the constraints of MessageData, but it would be really nice if it could produce linked constants without having to say the name of the constant (MessageData is lacking some kind of syntax equivalent to [this](foo.html)), which is very unfortunate for syntax references because they have horrible autogenerated names which are nevertheless useful for go-to-def.

[Mario Carneiro]

It's not actually markdown, only markdown-esque

[Mario Carneiro]

The printed docs are markdown though, so maybe making it markdown would help; but then it has issues with linking again

[David Thrane Christiansen]

Scott Morrison said:

David Thrane Christiansen, does this sound right? We do need an in-lean mechanism to look up all tactics / commands, I think.

We absolutely do! And an out-of-Lean one, for that matter.

My only real concern is preventing a proliferation of somewhat-compatible ways of documenting things (Markdown vs Verso markup vs MessageData). But that seems pretty solvable.

[David Thrane Christiansen]

The MessageData limitation that @Mario Carneiro pointed out seems pretty fixable, at least.

[David Thrane Christiansen]

All right, I just had a chat with @Marc Huisinga about this to see if there were any ways to provide this functionality over LSP, but we didn't come up with anything. A PR would be welcome!

[David Thrane Christiansen]

About the MessageData issue - can't the .ofPPFormat constructor be used to do what you're looking for? It needs a way to create a FormatWithInfos, which is a pretty-printer document paired with a map from Nat tags in the document to infotree nodes. Could this be used for what you're wanting to do, by ensuring there's just a single tag and a single node?

[Jason Rute]

This isn't tactics, but it's been pointed out on PA.SE that it is hard to figure out what noncomputable does. Hovering over it gives information for irreducible_def and help command "noncomputable" doesn't work either.