locating tactics and corresponding elaboration

Stream: metaprogramming / tactics

[Chris Henson]

I have two questions:

1) What is the recommended method of locating a tactic?
2) What is the recommended method of then locating the elaborator for that tactic?

For the first, I will somtimes do something like

#check `(by decide)

which for example would point me to docs#Lean.Parser.Tactic.decide.

Continuing with the example, how would I then in turn find docs#Lean.Elab.Tactic.evalDecide, which is in a different file? Ideally the solution would be generally applicable, but maybe this is an unusal example because it is a builtin tactic?

[Robin Arnez]

import Lean

example := by decide

and then ctrl+click on decide

[Chris Henson]

I am not getting a go to definition link to click on decide (and am also interested in what this looks like programmatically)

[Kevin Buzzard]

So just to clarify, if you copy the code Robin posted into VS Code, ignore the error, and ctrl+click on the word decide (or cmd+click on a mac) you don't jump to the definition of Lean.Elab.Tactic.evalDecide in core Lean?

[Chris Henson]

To clarify: if I include import Lean it does work, but not otherwise. Is this the expected behavior?

[Kyle Miller]

Yes, that's expected.

[Kyle Miller]

(Not ideal, but it's expected)

[Kyle Miller]

Both "go to definition" and "go to declaration" are useful for seeing the elaborator and the syntax definition.

[Kyle Miller]

I don't believe there's any resource for the programmatic solution except to read through source code for the LSP server. I think docs#Lean.Server.FileWorker.locationLinksOfInfo is the entry point for all the go-to-* logic.

[Chris Henson]

Thanks, that link is what I was about to ask for next! Is the reason that this doesn't work for decide until we import Lean because these definitions are in Init?

[Kyle Miller]

I think it's specifically because source position information hasn't been loaded in, and the source position is not a "builtin" (data that is in the Lean executable itself), instead it's just in the olean files and needs to be loaded. I'm not completely sure, I'd have to read through the source code.

Most projects will have enough of Lean imported for this data to be loaded.

[Kyle Miller]

Oh, it does work for decide. If you do "go to declaration" it goes to the syntax definition.

[Kyle Miller]

The issue you ran into is that "go to definition" goes to the elaborator that was invoked on the given syntax, but none of the Lean elaborator is in Init, so it hasn't been loaded, so there's no source position available for Lean.Elab.Tactic.evalDecide.

[Kyle Miller]

"The elaborator that was invoked" is important here: there's no direct mapping from syntax to an elaborator, and it's only resolved during tactic execution. There can be macros and multiple elaborators defined for a syntax, so you can't really know ahead of time what it will be. At least you can get the list of elaborators that it will try (maybe take a look at docs#Lean.Elab.Tactic.evalTactic to see how tactic evaluation works; there's some complexity in there you'll want to skip that's for incremental elaboration).

The reason "go to definition" works is that the LSP looks at data registered by withTacticInfoContext to determine which elaborator was executed for a given source syntax.