Confusing non-linear definitions of functions like`whnf`

Stream: lean4

[Jovan Gerbscheid]

There is a problem in lean when going to the definitions of whnf, inferType, isExprDefEqAux, isLevelDefEqAux, namely that they are opaque and have no reference to their definitions. I think the reaction of most newcomers trying to understand the code is that they cannot read these definitions anywhere. At least this was my reaction at first and I know I'm not the only one.

There is this comment:

/-! WARNING: The following 4 constants are a hack for simulating forward declarations.
   They are defined later using the `export` attribute. This is hackish because we
   have to hard-code the true arity of these definitions here, and make sure the C names match.
   We have used another hack based on `IO.Ref`s in the past, it was safer but less efficient. -/

I would much prefer it if the comment explicitly mentions the names whnfImp, inferTypeImp, isExprDefEqAuxImpl, isLevelDefEqAuxImpl.

[Eric Wieser]

Perhaps "goto definition" should also offer the implemented_by / export as the destination?

[Jovan Gerbscheid]

That would be great

[Mario Carneiro]

Eric Wieser said:

Perhaps "goto definition" should also offer the implemented_by / export as the destination?

That would indeed be great, I have long dreamed about implementing this, but it's pretty hard to get information about where externs are defined, because they could happen anywhere, including in C or C++ code

[James Gallicchio]

is there a way to get vscode-clickable links to other files, within a comment? then the comments could link to the files where they're defined, which requires manual maintenance but is better than status quo

[Mario Carneiro]

Not that I know of. Currently doc strings are not really broken up into link spans, which is actually kind of a problem because if you go-to-def on a docstring you often get a giant link to elabDeclaration

[James Gallicchio]

can we change that? :joy:

[Bolton Bailey]

It seems that you also get sent to elabDeclaration when you go-to-def on a declaration modifier like private or partial, which is annoying, firstly because the mouseover documentation on these modifiers is for Lean.Parser.Command.declModifiers, and secondly because neither of these are in the immediate vicinity of documentation for the actual purpose of the modifier in question.