Dependency Graph of Mathlib

Stream: mathlib4

[Shuffle]

Hi is there a way to build a dependency graph for all theorems, lemma and axioms in mathlib? I know https://github.com/leanprover-community/import-graph can build import graph for all lean files in mathlib.

I tried to implement one version,
graphExtractor2.lean
but in the extracted json file, theorem names seems weird, not the same as the original name
partial_dependency_graph2.json
For example, "private.Mathlib.Algebra.Group.End.0.Equiv.Perm.pow_aux.match_1".

What's wrong with my code and what is the correct way to get the real name of the theorems?

[Anne Baanen]

Names get mangled for two main reasons:

• Private declarations get a unique, very long prefix so they don't collide with other private declarations. I think you can just run docs#Lean.privateToUserName on all names and it will strip the unique prefix from any private names. That explains the first part of _private.Mathlib.Algebra.Group.End.0.Equiv.Perm.pow_aux.
• Declarations may contain other internal declarations (used for example in match blocks). Those internal details have suffixes on their names: see docs#Lean.Name.isImplementationDetail. I think there's some code that strips off those suffixes but I can't quickly find it.

[Jon Eugster]

Btw, this is not answering your question, but if you do get this working you could PR the functions getting the dependency graph of constants to import-graph, Maybe as something like ImportGraph/Constants.lean

I think that would be useful to have, but personally I don't have the bandwidth to add it myself.

[Shuffle]

Anne Baanen 发言道：

Names get mangled for two main reasons:

• Private declarations get a unique, very long prefix so they don't collide with other private declarations. I think you can just run docs#Lean.privateToUserName on all names and it will strip the unique prefix from any private names. That explains the first part of _private.Mathlib.Algebra.Group.End.0.Equiv.Perm.pow_aux.
• Declarations may contain other internal declarations (used for example in match blocks). Those internal details have suffixes on their names: see docs#Lean.Name.isImplementationDetail. I think there's some code that strips off those suffixes but I can't quickly find it.

Thanks! I will try if these could fix the bug.

[Shuffle]

Sure, I will let you know if I finish implementing this.

Jon Eugster 发言道：

Btw, this is not answering your question, but if you do get this working you could PR the functions getting the dependency graph of constants to import-graph, Maybe as something like ImportGraph/Constants.lean

I think that would be useful to have, but personally I don't have the bandwidth to add it myself.