Mimicking VSCode's "jump to definition" programmatically

Stream: lean4

[Shubhra Mishra]

I'm working on a project that requires me to programmatically extract Lean definitions. For example, if a proof uses add_comm, I want to retrieve the file containing the definition of add_comm. How can I do that? Thank you so much!

[Jon Eugster]

I think the infoview calls the RPC call Lean.Widget.getGoToLocation, so you can probably just do the same.

Maybe you can share a bit more which context your working in? I assume your project is written in Lean itself? In that case it shouldn't be too hard to follow the procedure above.

[Mario Carneiro]

import Mathlib.Algebra.Group.Basic

run_meta
  let some mod ← Lean.findModuleOf? ``add_comm | failure
  println! mod
  let some r ← Lean.findDeclarationRanges? ``add_comm | failure
  println! (r.range.pos, r.range.endPos)
-- Mathlib.Algebra.Group.Defs
-- (⟨297, 2⟩, ⟨297, 13⟩)

[Mario Carneiro]

note that line 297:2-13 of Mathlib/Algebra/Group/Basic.lean is actually the text to_additive in

@[to_additive]
theorem mul_comm : ∀ a b : G, a * b = b * a := CommMagma.mul_comm

because add_comm is not defined directly, it is generated by additivizing mul_comm

[Shubhra Mishra]

Ah, I see. Thank you for pointing that out, Mario! And @Jon Eugster, the idea I'm interested in experimenting with is how language models can self-improve on their Lean capabilities. Obviously, given how much LLMs hallucinate, pure self-improvement (without absolutely any ground truth) wouldn't work. So I wanted to see how LLMs would perform if I gave them a theorem statement (in Lean), and asked them to generate the proof, but also provided documentation related to the proof. I was planning on using theorems/proofs from MathLib4, meaning that this documentation I provide could just be the code containing the other theorems called on in intermediate steps for the ground truth mathlib4 proof. It's totally possible that self-improving this way would perform even worse than simply finetuning on mathlib4, but it was an experiment I was curious to run. The framework I have so far is in Python (as I've never used Lean to actually program, haha). But would you recommend using Lean instead? And thanks for all your help!