(bug?) handleDocumentSymbol does not work for lemmas

Stream: lean4

[Lua Viana Reis]

I noticed that the LSP textDocument/documentSymbol request is not returning mathlib's lemmas among the other declarations. For instance, you can check that in VSCode by clicking the three dots in the header line:

image.png

I'm curious whether this bug is in the mathlib side or Lean's side. It seems mathlib is properly expanding lemma to theorem and marking the lemma as a declaration, but somehow it's still not visible to the server?

[Lua Viana Reis]

It seems the problem is in the Lean side, because foo below also does not show:

macro "stupid" dec:command : command => pure dec

stupid theorem foo : 1 = 1 := rfl

[Robin Arnez]

Well it only cares about docs#Lean.Parser.Command.declaration​s and lemma isn't a declaration, nor is your "stupid" macro

[Lua Viana Reis]

@Robin Arnez I don't think this is (exactly) the issue. If you look at the source of lemma in Mathlib, it does change the syntax kind. But perhaps the syntax after macro expansion is not considered

[Robin Arnez]

Yeah that's what I mean. It looks at the original syntax and docs#lemma != docs#Lean.Parser.Command.declaration

[Lua Viana Reis]

wouldn't it be desirable to apply macro expansion too? I found the fact lemmas are not reported a bit annoying, especially in Emacs where I like to navigate the file with imenu (which is like a TOC)

[Lua Viana Reis]

it also does not work with open [identifier] in [command] syntax. Leading to the slightly ironic fact that handleDocumentSymbol is not listing itself

[Kyle Miller]

Looks like a bug to me. (I think Robin is just explaining the error, not justifying it.)

Want to report it on Github if it's not already there? https://github.com/leanprover/lean4/issues

[Lua Viana Reis]

I'm trying to learn more about Lean's internals, so I attempted an implementation myself

but I'll try to report the issue there, I'm not sure if my way is the "right" way (via Snapshot.infoTree)

[Lua Viana Reis]

if I import it in another file, everything shows up in the list

code

import Lean.Server.Requests
import Lean.Elab.BuiltinCommand
import Lean.Elab.Declaration

open Lean Server RequestM Lsp Elab

partial def handleDocumentSymbol (_ : DocumentSymbolParams) (_ : RequestTask DocumentSymbolResult)
    : RequestM (RequestTask DocumentSymbolResult) := do
  let doc ← readDoc
  -- bad: we have to wait on elaboration of the entire file before we can report document symbols
  let t := doc.cmdSnaps.waitAll
  mapTaskCostly t fun (snaps, _) => do
    let syms := snaps.map (·.infoTree) |> toDocumentSymbols doc.meta.text #[]
    return { syms := syms }
where
  mkLevel text syms its up range (id : Option (TSyntax `ident)) :=
    let up stop its children :=
      let sym := DocumentSymbol.mk {
        name := id.elim "<section>" (·.getId.toString)
        kind := .namespace
        range := {range with stop}.toLspRange text
        selectionRange := id.elim range (·.raw.getRange?.get!) |>.toLspRange text
        children? := .some children
      }
      toDocumentSymbols text (syms.push sym) its up
    toDocumentSymbols text #[] its up

  toDocumentSymbols (text : FileMap) (syms : Array DocumentSymbol) (its : List InfoTree)
      (up : String.Pos → List InfoTree → Array DocumentSymbol → Array DocumentSymbol := λ _ _ a ↦ a) :
      Array DocumentSymbol :=
    match its with
    | it :: its =>
      match it with
      | .context _ it => toDocumentSymbols text syms (it :: its) up
      | .node (.ofCommandInfo {elaborator, stx}) children => Id.run do
        let range := stx.getRange?.getD ⟨0,0⟩
        match elaborator with
        | ``Command.elabNamespace =>
          if let `(namespace $id) := stx then
            return mkLevel text syms its up range id
        | ``Command.elabSection =>
          if let `($_:sectionHeader section $(id)?) := stx then
            return mkLevel text syms its up range id
        | ``Command.elabEnd =>
          return up stx.getRange?.get!.stop its syms
        | ``Command.elabDeclaration =>
          if let some stxRange := stx.getRange? then
            let (name, selection) := match stx with
              | `($_:declModifiers $_:attrKind instance $[$np:namedPrio]? $[$id$[.{$ls,*}]?]? $sig:declSig $_) =>
                ((·.getId.toString) <$> id |>.getD s!"instance {sig.raw.reprint.getD ""}", id.map (·.raw) |>.getD sig)
              | _ =>
                match stx.getArg 1 |>.getArg 1 with
                | `(declId|$id$[.{$ls,*}]?) => (id.raw.getId.toString, id)
                | _ =>
                  let stx10 := stx[1][0]
                  (stx10.isIdOrAtom?.getD "<unknown>", stx10)
            if let some selRange := selection.getRange? then
              let sym := DocumentSymbol.mk {
                name := name
                kind := SymbolKind.method
                range := stxRange.toLspRange text
                selectionRange := selRange.toLspRange text
              }
              return toDocumentSymbols text (syms.push sym) its up
        | (_ : Name) => pure ()
        toDocumentSymbols text syms (children.toList ++ its) up
      | .node _ children => toDocumentSymbols text syms (children.toList ++ its) up
      | .hole _ => toDocumentSymbols text syms its up
    | [] => up text.source.endPos [] syms

deriving instance FromJson for DocumentSymbol
deriving instance FromJson for DocumentSymbolResult

initialize
  chainLspRequestHandler
    "textDocument/documentSymbol"
    DocumentSymbolParams
    DocumentSymbolResult
    handleDocumentSymbol

edit: I made an issue lean4#10190

[Lua Viana Reis]

@Kyle Miller do you think I could turn this implementation into a PR?

[Kyle Miller]

Let's ping @Marc Huisinga about this issue (lean4#10190), since he's responsible for LSP.

[Robin Arnez]

I don't think the elaborator is a good thing to look at since the syntax may be completely different before macro expansion. I'd simply try macro expanding the syntax (or reading macro expansion info?) but I'm not sure how exactly you'd be able to do that in RequestM

[Lua Viana Reis]

Do you have an example in mind of how different it could be? From my usage so far, only autogenerated identifiers sometimes look odd in the listing

[Lua Viana Reis]

and I think think this would be the biggest possible problem, for only the source position and identifier of the declaration are taken into account for the document symbols

[Robin Arnez]

I believe the stupid macro would already break the elaborator approach since you'd be looking at the wrong syntax, so it'd look at theorem foo : 1 = 1 := rfl instead of foo

[Robin Arnez]

and then you just get <unknown>

[Lua Viana Reis]

but in what sense it would "break" it? this is how it is reported with the patch:

image.png

[Lua Viana Reis]

personally, I like that the declarations with autogenerated names are listed as well

[Robin Arnez]

Hmm, does it work with

macro "slightly" "stupid" dec:command : command => pure dec

slightly stupid theorem abc : 1 = 1 := rfl

too?

[Robin Arnez]

Oh wait are you looking at the info tree? I already wondered how you do that lol

[Lua Viana Reis]

image.png

[Robin Arnez]

I guess maybe this approach does work then? I'm not too sure though, let's wait on what @Marc Huisinga thinks about this

[Marc Huisinga]

I'd be happy to review a PR that fixes this issue. Having some tests for this feature would also be great.
Note that since the document symbols request is used for all kinds of UI features, not just the symbol search, it should attempt to not report any redundant entries.

In the future, we may also still need to rewrite this feature entirely so that it doesn't have to wait for the full elaboration of the entire file anymore.

[Lua Viana Reis]

Thanks @Marc Huisinga :-) I have two questions:

• What is the criterion for redundancy? In the example above, the macro expands to two named declarations. Should it report only one since they belong to the same position in the file? And if so, which one? Personally, I prefer both declarations to be listed.
• When you say it could be rewritten not to wait for the exaboration of the entire file, what is the idea here? To only apply macro expansion to the syntax, or to use some sort of cache?

[Lua Viana Reis]

Perhaps another question that should be considered first:

• What should count as an entry in the symbols list? Currently, it's a declaration, because they usually have names. That said, there is a special case for unnamed instances, which show up as instance : type annotation in the list. Perhaps, we could add special cases for macros and syntaxs which often are not explicitely named as well.

[Lua Viana Reis]

Another idea would be to explicitely have a class IsDocumentSymbol Name for some syntax nodes, which could be instantiated by providing the way to get the name and position from the syntax.

[Lua Viana Reis]

@Marc Huisinga I had this code sitting here for a while (I'm using it as a server plugin), so I made a PR lean4#11228. I think the questions above are still valid, so feel free to modify or close it, but I'm still making a case for it as in Emacs having the symbols is very very convenient for jumping around the file fast.

[Lua Viana Reis]

Marc Huisinga said:

In the future, we may also still need to rewrite this feature entirely so that it doesn't have to wait for the full elaboration of the entire file anymore.

Do you mean, report a partial list of symbols during elaboration?