fix: attribute info nesting

[digama0]

This fixes an issue with hovers inside user attributes caused by the fact that the info nodes generated by the user attribute are not nested correctly under the attribute itself, owing to the fact that the info node for the attribute itself is generated at elaboration time while the info nodes generated by the attribute are added at application time, which may be much later.

Now the attribute node is generated immediately before the user function is called, and the nodes generated by the user code nest inside the attribute node.

It is difficult to add a test case for this, though, since all of the tests/lean/interactive tests are single-file and none of the builtin attributes add an info span over the attribute name (which is where the original bug manifests). This was extracted from this mathlib4 issue.

import Lean
open Lean Elab

syntax (name := test) "test" ident : attr

initialize registerBuiltinAttribute {
    name := `test
    descr := "test"
    add := fun decl stx _ => do
      pushInfoLeaf <| .ofTermInfo {
        elaborator := .anonymous, lctx := {}, expectedType? := none
        stx := stx[0]
        expr := (← mkConstWithLevelParams decl)
      }
  }

import Test.Attr

/-- doc -/
@[test x] def foo := 1
--^ textDocument/hover
-- should show "foo : Nat" instead of fooAttr

[leodemoura]

@Kha Do you see a quick hack to add the test @digama0 provided above to our test suite?

[Kha]

Not really, no.

[Kha]

This fixes an issue with hovers inside user attributes caused by the fact that the info nodes generated by the user attribute are not nested correctly under the attribute itself

Is this resolved by https://github.com/leanprover/lean4/pull/1753/files#diff-83bd7ca17a546fdf495692949c7412fc3a059f292c59e667898804da030dba22R156-R160?

[Kha]

I think we concluded last week that we can merge this?