Find the package where the dependencies from in lean.

Stream: general

[Jiashuo Zhang]

Hi, I’m new to Lean metaprogramming and I’m working on building a dependency graph.
In addition to collecting the dependencies (lemmas), I’d like to also record the source of each lemma — specifically, which package/file and location it comes from (similar to how VS Code hover shows import Mathlib.**). I believe this might be available via the Lean Server Protocol.

I haven’t seen this functionality in existing tools (e.g. lean-graph).
Does anyone know how I could implement this?

[Aaron Liu]

Like this?

Aaron Liu said:

Aaron Liu said:

import Mathlib

open Lean

run_cmd do
  let env ← getEnv
  let name := ``add_comm
  let module? := env.getModuleFor? name
  logInfo m!"{module?}" -- some (Mathlib.Algebra.Group.Defs)
  let name := `not_a_theorem
  let module? := env.getModuleFor? name
  logInfo m!"{module?}" -- none

[Jiashuo Zhang]

Aaron Liu 发言道：

Like this?

Aaron Liu said:

Aaron Liu said:

import Mathlib

open Lean

run_cmd do
  let env ← getEnv
  let name := ``add_comm
  let module? := env.getModuleFor? name
  logInfo m!"{module?}" -- some (Mathlib.Algebra.Group.Defs)
  let name := `not_a_theorem
  let module? := env.getModuleFor? name
  logInfo m!"{module?}" -- none

That’s exactly what I was looking for — thank you so much for your help! :folded_hands: