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: