syntax and elaboration functions are nowhere near each other

Stream: lean4

[Mario Carneiro]

This is a bit of a recurring problem for me and possibly others. Suppose I want to know how the #eval command works. Currently I can search lean for "#eval, although I can also imagine go-to-definition working for this as well, and this takes me to the syntax definition for #eval, a line like this:

@[builtinCommandParser] def eval := parser! "#eval " >> termParser

As a user, the step after this is not so obvious. This is just the definition of the syntax, and the elaborator is not in the same file or in some other obviously related place. To find the actual elaborator, one has to search for «eval» (which is not easy to write in vscode search unless you have abbreviations via an IME like Gabriel Ebner ), or more specifically @[builtinCommandElab «eval»], to find the elaborator for this syntax.

1. Why are the two parts so widely separated? Is this a requirement due to staging? If they were adjacent in the file then the relation from one to the other would be more easily discoverable.
2. Assuming the separation is necessary, could we get something like go-to-definition to work to follow the syntax -> elaborator path? We could repurpose one of vscode's "go to declaration" / "go to type definition" commands although that's a bit of abuse, or add some other LSP extension to allow someone to go between def eval := ... and @[builtinCommandElab «eval»] def elabEval := ....

Personally I would prefer option 1. This same issue can afflict lean 3 as well, if the declaration of a notation is widely separated from the definition, but for the most part they come one after another, with the only exception being the declarations of infix notations like + in core, where the two parts are separated by 100 lines in the same file.

[Gabriel Ebner]

I think the standard way to do this in LSP is to show multiple locations in the go-to-definition command. For example the typescript language server will give two locations if you want to go to foo(42):

const foo = x => x+1;
module.exports = {foo};

You then need to select which one you want (vscode even shows a nice preview). There are also other places where we might want to have multiple go-to-definition destinations: e.g. x + 1 might show the Add type class, the Nat instance, and the notation.

[Sebastian Ullrich]

Mario Carneiro said:

Why are the two parts so widely separated? Is this a requirement due to staging?

No; in fact we started running the parsers of the current stage in syntax quotations using the interpreter so we can change syntax and semantics at the same time. But it's hard to consistently shape a grammar when there are hundreds of lines of elaboration code between the syntax rules.

2. Assuming the separation is necessary, could we get something like go-to-definition to work to follow the syntax -> elaborator path?

My thinking so far was to have go-to-definition on (unquoted) syntax go to the elaborator, since there can be multiple elaborators for the same syntax kind. From there, clicking on the attribute parameter or quoted syntax should bring you to the parser. Going from the parser to the elaborator is not really feasible since it's a forward reference.

The hover docstring as well should be taken from the elaborator since again there can be multiple elaborators implementing different semantics, and because docstrings would again blow up the grammar.