Ranges for Go-to-definition

Stream: lean4

[Damiano Testa]

In the code below, if I Ctrl-Click on in I get redirected to the elaborator for the command in.

Where is the information about the ranges for such redirection? How can I access these ranges?

Thanks!

import Lean

open Nat in
/-!-/

[Sebastian Ullrich]

It's just the range of the entire in syntax node, at least where it is not covered by ranges of subcommands. There is no explicit range for the token in itself being used.

[Damiano Testa]

Yes, I imagined that this is what it was, but where can I access those ranges?

[Sebastian Ullrich]

Syntax.getRange?

[Damiano Testa]

I suspect that, when Lean parses the file, it stores somewhere this information and I would like to know where and how can I retrieve it.

[Damiano Testa]

Ok, so then were can I retrieve the syntax for the file?

[Sebastian Ullrich]

I assume you know how to get the syntax of the current command? Your example does not make clear whether you need more. Only the server currently knows the syntax tree of the entire file.

[Damiano Testa]

What I have is a list of declaration names. Looking at the declarationRange extension, I can retrieve the ranges for the corresponding declarations. However, I would like to get the ranges for the commands that created those declarations.

[Damiano Testa]

Is there some way to obtain that?

[Damiano Testa]

In the example above, I can retrieve the ranges for the module doc, but I would really like to have the ranges for in.

[Sebastian Ullrich]

That's not persisted anywhere, no

[Damiano Testa]

Ok, so what is the mechanism that Go to definition uses?

[Sebastian Ullrich]

As I said, the server has that information. Other components don't.

[Damiano Testa]

I do not actually know what the server is, but I gather that it is not something that lean can access?

[Damiano Testa]

And so the process is that lean parses the file, temporarily creates the syntax of every command, passes (some of) the information to the server and then discards it?

[Robin Arnez]

You can kinda redo what the server does though:

import Lean

open Lean Parser

def fullReparse : CoreM (TSyntax `Lean.Parser.Module.header × Array Command) := do
  let fileMap ← getFileMap
  let fileName ← getFileName
  let ictx : InputContext := {
    input := fileMap.source
    fileName
    fileMap
  }
  let (header, state, messages) ← parseHeader ictx
  let pmctx : ParserModuleContext := {
    env := ← getEnv
    options := ← getOptions
    currNamespace := ← getCurrNamespace
    openDecls := ← getOpenDecls
  }
  let mut state := state
  let mut messages := messages
  let mut cmds := #[]
  repeat
    if fileMap.source.atEnd state.pos then
      break
    let (stx, newState, newMessages) := parseCommand ictx pmctx state messages
    state := newState
    messages := newMessages
    cmds := cmds.push ⟨stx⟩
  return (header, cmds)

def whereAmI : CoreM (Option Command) := do
  let (_header, cmds) ← fullReparse
  let ref ← getRef
  let some range := ref.getRange? | return none
  for c in cmds do
    let some cmdRange := c.raw.getRange? | continue
    if cmdRange.includes range then
      return some c
  return none

elab "whereami" : tactic => do
  let some cmd ← whereAmI | throwError "no position found"
  Lean.logInfo cmd

example : True := by
  whereami

although this might not be fully accurate if there are syntax commands in between

[Sebastian Ullrich]

Rather it will just fail on any file with notations, so please don't

[Damiano Testa]

For my use-case, it is simpler to add a linter that simply emits the ranges of every command that it inspects.

[Damiano Testa]

I was simply hoping to be able to avoid having to rebuild each file, since at some point, the information that I want is computed.

[Damiano Testa]

To give some context: I am trying to write automation to remove "old" deprecated declarations. For this, I can look in the environment to find

• which declarations have been deprecated in any given range of time (according to the since value);
• find the ranges of the declarations in their files;
• remove these ranges from the files.

This process fails if there is something like

set_option linter.deprecated false in
@[deprecated (since := "2025-02-30")] alias N := Nat

because the set_option line would be left dangling (and would apply to the following command, if there is one).

[Damiano Testa]

If, instead, I can retrieve the command ranges that have generated the declarations, then I am done!

[Damiano Testa]

Currently, it seems that the simplest approach is to have a re-parsing step where a linter logs all the command ranges, and then use this information to remove the emitted command ranges that entirely contain the declaration ranges that I want to remove.

[Robin Arnez]

Sebastian Ullrich schrieb:

Rather it will just fail on any file with notations, so please don't

I believe it will still work as long as you take the environment from the end of the file but there are definitely some edge cases

[Damiano Testa]

Would the code not complain about existing declarations, if you use the end environment?

[Robin Arnez]

I mean it's just parsing; the parser doesn't care

[Damiano Testa]

Ah, ok, I thought that you were re-building all the file.

[Damiano Testa]

Anyway, maybe I can use the linter emitting ranges to emit more information as well and re-purpose it for more than just figuring out if there is an in before a declaration.

[Damiano Testa]

At least if feels less wasteful like this! :slight_smile: