go to definition for `open`

Stream: lean4

[Julian Berman]

Is there an easy-to-implement better target that go to definition could jump to for open Foo Bar Baz? Without considering how possible this is it would be amazing if clicking on Bar jumped you either to a declaration Bar or else to the namespace Bar command which is highest in the import graph.

Maybe there's a simpler place that's still reasonable? Right now it takes you to the definition of elabOpen.

[Damiano Testa]

I think that namespaces register themselves in an environment extension and maybe you can retrieve where that happened. I am not sure.

[Damiano Testa]

Thinking a bit about this, I don't think that the environment extension remembers where the namespace was added. However, you could search the environment for all declarations that have the given namespace, selects a minimal one in import order and then give the location of that declaration.

[Kenny Lau]

do you have the code where the env ext was initialised?

[Kenny Lau]

ok it seems to be here: https://github.com/leanprover/lean4/blob/f1203f3d0d4f330ceb63dfce0f11d4fec7598755/src/Lean/Namespace.lean#L18C70-L18C78

(very suspicious, it has a namespace command right above it)

[Kenny Lau]

and it does seem to only store the Name, so it wouldn't store the Syntax that contains the cursor position

[Kenny Lau]

actually, are we sure that Lean.SimplePersistentEnvExtension does not store any position information at all?

[Damiano Testa]

I don't know if there is no position stored, but the declRanges extension does store position information. You can access that, once you know what the declaration is.

[Damiano Testa]

I am not sure if I trust the namespace_where command below much, however namespace_where YourNamespace should return "something". Ideally, it is a list of import-minimal modules containing a declaration that has YourNamespace as a component and also the first declaration in the file that contains the namespace. The declaration name is control-clickable.

import Mathlib.Lean.Expr.Basic

open Lean

/-- The `<` partial order on modules: `importLT env mod₁ mod₂` means that `mod₂` imports `mod₁`. -/
def SortImports.importLT (env : Environment) (f1 f2 : Name) : Bool :=
  (env.findRedundantImports #[f1, f2]).contains f1

open Lean Elab Command in
elab "namespace_where " ns:ident : command => do
  let part := ns.getId
  -- The collection of module names of declarations that contain `ns` as a component.
  let mut candidateModules : NameSet := ∅
  let env ← getEnv
  -- The collection of names of declarations that contain `ns` as a component.
  let mut goodNames : NameSet := ∅
  -- We first loop through the constants in the environment, searching for non-blacklisted
  -- names that contain the given namespace as a component.
  for (n, _) in env.constants.map₁ do
    if ← n.isBlackListed then continue
    if n.components.contains part then
      let some mod ← findModuleOf? n | throwError "Could not find module of {n}"
      candidateModules := candidateModules.insert mod
      goodNames := goodNames.insert n
  let currMod ← getMainModule
  -- We do the same loop, but over the constants in the current file.
  for (n, _) in env.constants.map₂ do
    if ← n.isBlackListed then continue
    if n.components.contains part then
      candidateModules := candidateModules.insert currMod
      goodNames := goodNames.insert n
  let minimalImports := env.findRedundantImports candidateModules.toArray
  -- This should make the command do the right thing if the namespace appears
  -- only in the current file only
  let minimalImports := if minimalImports.isEmpty then {currMod} else minimalImports
  let minimals := candidateModules.filter minimalImports.contains
  let sorted := minimals.toArray.qsort (SortImports.importLT env)
  let sortDecls := sorted.map fun mod => (mod,
    let extArray :=
      if let some modIdx := env.getModuleIdx? mod then
        declRangeExt.getModuleEntries env modIdx
      else
        (declRangeExt.getState env).toArray
    let extn := extArray.qsort (·.2.range.pos.line < ·.2.range.pos.line)
    extn.filterMap fun (nm, rgs) =>
      if goodNames.contains nm then
        some (nm, rgs.range.pos)
      else
        none)
  logInfo <| m!"\n".joinSep (sortDecls.filterMap fun (mod, nms) =>
    if let some (nm, _) := nms[0]?
    then
      some (m!"\nModule: {mod}{indentD <| .ofConstName nm}")
    else none).toList

namespace_where Grind

theorem X.A : True := trivial
theorem X.B : True := trivial
theorem X.C : True := trivial

namespace_where X