RFC: Jump to declaration in #where

Stream: lean4

[Yaël Dillies]

I often find myself searching for the place where a specific typeclass assumption has been declared in a large file. This is time-consuming and I was hoping #where would help, but #where only ever tells you what's declared at a specific point in the file, rather than where it was declared. Would it be possible to make the log info printed by #where clickable, so that each part of it gives the place where the syntax was declared?

[Eric Wieser]

As in, jump to the variable line?

[Yaël Dillies]

... or the set_option ... or the noncomputable section or ...

[Damiano Testa]

I don't really know how to get the "jump to definition" part, but for variables, the position information is stored in the scope, so you can at least make them "visible":

import Lean

open Lean Elab Command

elab "#where!" : command => do
  let s ← getScope
  let vars := s.varDecls
  let fm ← getFileMap
  let mut msg := #[]
  for v in vars do
    let pos := fm.toPosition (v.raw.getPos?.getD default)
    msg := msg.push m!"Line {pos.line}, column {pos.column}: {(v.raw.getSubstring?.getD default).trim}"
    logInfoAt v m!"{pos}: {(v.raw.getSubstring?.getD default).trim}"
  logInfo <| m!"\n".joinSep msg.toList

open Nat in
variable (x y : Nat)

variable (x y : Nat)

variable (z w : Nat) (a : Unit)

/--
info: ⟨19, 9⟩: (x y : Nat)
---
info: ⟨21, 9⟩: (z w : Nat)
---
info: ⟨21, 21⟩: (a : Unit)
---
info: Line 19, column 9: (x y : Nat)
Line 21, column 9: (z w : Nat)
Line 21, column 21: (a : Unit)
-/
#guard_msgs in
#where!

[Damiano Testa]

In the code above, each variable command is highlighted (except that #guard_msgs "captures" the highlight). The "individual" messages are logged at the corresponding variable location. while the final "summary" is on the #where! syntax..