Import position of ConstInfo

Stream: Is there code for X?

[Joachim Breitner]

Maybe I’m too tired, but given a ConstInfo, how do I find the module it was defined in? Maybe even the source position?
And are Lean.ModuleIdx assigned sequentially, i.e. can I use them to topologically sort modules in the import graph?

[Henrik Böving]

You can get the source position of any name with Lean.findDeclarationRanges?

[Henrik Böving]

and for getting the module the environment maintains a field const2ModIdx that you can use

[Joachim Breitner]

Thanks! And looks sequential: https://github.com/leanprover/lean4/blob/869d64e97ac5acf557c949c2af917db633999f8d/src/Lean/Environment.lean#L757
Will play with this to better sort in loogle at some point.

[Adam Topaz]

I've used the following code for something similar (for the module name) in the past:

def getModuleNameFor? (env : Environment) (nm : Name) : Option Name :=
  env.getModuleIdxFor? nm >>= fun i => env.header.moduleNames[i.toNat]?