Zulip Chat Archive

Stream: new members

Topic: Finding joins in the module graph

Joachim Breitner (Feb 24 2022 at 08:27):

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 (Feb 24 2022 at 08:32):

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 (Feb 24 2022 at 08:52):

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

Mario Carneiro (Feb 24 2022 at 08:59):

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

Eric Wieser (Feb 24 2022 at 11:07):

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

Joachim Breitner (Feb 24 2022 at 13:43):

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 (Feb 24 2022 at 14:33):

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 (Feb 24 2022 at 14:34):

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

Alex J. Best (Feb 24 2022 at 14:38):

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

Joachim Breitner (Mar 10 2022 at 16:33):

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

Last updated: Dec 20 2023 at 11:08 UTC