Programmatically determining where a constant is defined

Stream: new members

[Louis Cabarion]

Given a constant name—say mul_assoc—how can I programmatically determine where it is defined?

Is there a command (for example, something like #which mul_assoc) that would report this?

For the mul_assoc example I’d like to get Mathlib.Algebra.Group.Defs ideally together with the line number.

[Aaron Liu]

I answered this question already, let me pull that up

[Aaron Liu]

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

[Aaron Liu]

I'm not sure how to get the line number though

[Damiano Testa]

You can get line numbers from the DeclarationsRangeExtension. I'm on mobile, though.

[Damiano Testa]

There should also already be a thread with such a function in #lean4 somewhere: maybe searching there for messages sent by me and containing the name of the extension may yield it.

[Aaron Liu]

Found it: #lean4 > Return definition of a declaration? @ 💬

[Louis Cabarion]

Isak Colboubrani said:

For the mul_assoc example I’d like to get Mathlib.Algebra.Group.Defs ideally together with the line number.

Upon reflection, the (module, line number) pair doesn’t make sense -- modules may be spread across several files, but line numbers are file-specific.

[Louis Cabarion]

Thanks Damiano and Aaron!

As a first step I managed to create a #loc <identifier> command that returns the number of lines in an identifier’s definition. Code review request: any tips for making this code more idiomatic are welcome.

import Mathlib

elab "#loc" identifier:ident : command => do
  let name := identifier.getId
  match ← Lean.findDeclarationRanges? name with
  | some declarationRanges =>
    let range := declarationRanges.range
    let lines := 1 + range.endPos.line - range.pos.line
    Lean.logInfo m!"Lines of code for '{name}': {lines}"
  | none => Lean.logInfo m!"unknown identifier '{name}'"

#loc mul_assoc
-- Output:
-- Lines of code for 'mul_assoc': 3

[Damiano Testa]

If you use

  let name ← liftCoreM do Lean.realizeGlobalConstNoOverload identifier

instead of simply getting the identifier, then you leave the error management of what happens when the constant does not exist to the core functions.

[Damiano Testa]

Also, using

    Lean.logInfo m!"Lines of code for '{.ofConstName name}': {lines}"

with .ofConstName, makes the name clickable in the infoview.

[Damiano Testa]

So, you could compress your code to

open Lean Elab Command in
elab "#loc" identifier:ident : command => do
  let name ← liftCoreM do Lean.realizeGlobalConstNoOverload identifier
  if let some {range := range, ..} ← Lean.findDeclarationRanges? name then
    let lines := 1 + range.endPos.line - range.pos.line
    Lean.logInfo m!"Lines of code for '{.ofConstName name}': {lines}"

[Aaron Liu]

Isak Colboubrani said:

Isak Colboubrani said:

For the mul_assoc example I’d like to get Mathlib.Algebra.Group.Defs ideally together with the line number.

Upon reflection, the (module, line number) pair doesn’t make sense -- modules may be spread across several files, but line numbers are file-specific.

I'm going through most of mathlib right now and so far all the modules are one file.

[Damiano Testa]

I don't think that there is a distinction between module and file. What would it be?

[Louis Cabarion]

Apologies -- I conflated modules and namespaces. There exists a bijection between the set of files and the set of modules (whereas the correspondence between files and namespaces is a non-functional, many-to-many relation).

Thus, a pair of the form (module, line number) uniquely identifies a location in the code , whereas a pair (namespace, line number) does not (since namespaces may span multiple files).

[Louis Cabarion]

Thanks for the code review @Damiano Testa!

This is my current version:

import Mathlib

open Lean Elab Command in
elab "#loc" identifier:ident : command => do
  let name ← liftCoreM do Lean.realizeGlobalConstNoOverload identifier
  if let some {range := range, ..} ← Lean.findDeclarationRanges? name then
    let lines := 1 + range.endPos.line - range.pos.line
    Lean.logInfo m!"Lines of code for '{.ofConstName name}': {lines}"
  else
    Lean.logInfo m!"Cannot compute lines of code for '{.ofConstName name}'"

Please let me know if anything can be improved further.

[Louis Cabarion]

I ran into an unexpected issue: it seems like Lean.findDeclarationRanges fails for MvPFunctor.WPath.root.inj.

Example:

-- Works:
#loc mul_assoc
-- Lines of code for 'mul_assoc': 3
#check mul_assoc
-- mul_assoc.{u_1} {G : Type u_1} [Semigroup G] (a b c : G) …

-- Does not work:
#loc MvPFunctor.WPath.root.inj
-- Unknown line count for 'MvPFunctor.WPath.root.inj'
#check MvPFunctor.WPath.root.inj
-- MvPFunctor.WPath.root.inj.{u} {n : ℕ} …

What is special about MvPFunctor.WPath.root.inj?

[Damiano Testa]

docs#MvPFunctor.WPath.root.inj
docs#MvPFunctor.WPath.root

[Damiano Testa]

It looks like docs#MvPFunctor.WPath.root.inj is not a declaration.

[Aaron Liu]

MvPFunctor.WPath.root.inj is the automatically generated injectivity theorem for the constructor MvPFunctor.WPath.root. Compare with, for example, Nat.succ.inj.

[Louis Cabarion]

Thanks -- TIL! Is it precisely for automatically generated code that this behavior will be triggered, or can anyone think of other scenarios in which Lean.findDeclarationRanges might fail (given an existing identifier name acquired via let name ← liftCoreM do Lean.realizeGlobalConstNoOverload identifier)?

[Aaron Liu]

Maybe on stuff like docs#UInt8.zero_def which was generated by a command?

[Aaron Liu]

Interestingly, #loc Nat.succ.inj does work, as well as #loc Nat.succ.injEq and #loc Nat.noConfusion.

[Louis Cabarion]

Thanks @Aaron Liu. That's a bit surprising. I can’t see the exact pattern separating the working cases from the failing ones with regards to Lean.findDeclarationRanges (and thus line numbers). In each case, however, the module name (env.getModuleFor) is reported correctly.

These are some working and non-working examples:

• UInt8.zero_def works (line number is reported), List.reverseRecOn.eq_def does not.
• Nat.noConfusion works, NatPowAssoc.noConfusionType does not.
• Nat.succ.injEq works, AbsoluteValue.mk.injEq does not.
• Nat.succ.inj works, DihedralGroup.r.inj does not.

#mwe

import Mathlib

open Lean Elab Command in
elab "#loc" identifier:ident : command => do
  let name ← liftCoreM do Lean.realizeGlobalConstNoOverload identifier
  if let some {range := range, ..} ← Lean.findDeclarationRanges? name then
    let lines := 1 + range.endPos.line - range.pos.line
    Lean.logInfo m!"Lines of code for '{.ofConstName name}': {lines}"
  else
    Lean.logInfo m!"Cannot compute lines of code for '{.ofConstName name}'"

#loc UInt8.zero_def -- Lines of code for 'UInt8.zero_def': 1
#loc List.reverseRecOn.eq_def -- Cannot compute lines of code for 'List.reverseRecOn.eq_def'
#loc Nat.noConfusion -- Lines of code for 'Nat.noConfusion': 22
#loc NatPowAssoc.noConfusionType -- Cannot compute lines of code for 'NatPowAssoc.noConfusionType'
#loc Nat.succ.injEq -- Lines of code for 'Nat.succ.injEq': 2
#loc AbsoluteValue.mk.injEq -- Cannot compute lines of code for 'AbsoluteValue.mk.injEq'
#loc Nat.succ.inj -- Lines of code for 'Nat.succ.inj': 2
#loc DihedralGroup.r.inj -- Cannot compute lines of code for 'DihedralGroup.r.inj'