Finding joins in the module graph

Stream: new members

[Joachim Breitner]

Assume I have a helper lemma that combines two concepts (in this case, nat.coprime.mul and finset.prod), and I need to find the right module to put this. Is there a tool that helps me with that? Something that might tell me “All modules depending on both data.nat.gcd and algebra.big_operators.basic also depend on module X”, so that X is the natural home for such a lemma?

[Eric Wieser]

If you're familiar with Python and networkx, there's a dependency graph that you can read in available at https://leanprover-community.github.io/mathlib_docs/import.gexf

[Patrick Massot]

Note that leanproject will also create such a graph for you: leanproject import-graph --help

[Mario Carneiro]

Is there an easy way to read this back into lean?

[Eric Wieser]

I've found in the past that leanproject import-graph is painfully slow - but maybe you just need a clean working tree

[Joachim Breitner]

I vaguely recall that for Isabelle I once wrote a command that would suggest which module to move a theorem to, that may be possible in lean too, but that would only consider modules that are already imported, so a bit less useful.

[Alex J. Best]

There is a prototype of this at https://github.com/alexjbest/dag-tools/blob/master/src/home_finder.lean it is a bit slow but more or less works iirc

[Alex J. Best]

It's called #vind_home to avoid conflict with #find lol

[Alex J. Best]

Demo is at https://github.com/alexjbest/dag-tools/blob/master/src/test_home_finder.lean

[Joachim Breitner]

JFTR (or just-for-the-web-archive-if-someone-googles-this-thread), as I randomly stumbled over it: My experiments with such a tool in Isabelle are in https://github.com/nomeata/isa-where-to-move