Transitive imports

Stream: new members

[Martin Dvořák]

If your file B requires A and your file C requires both A and B, what do you write as import in the file C? Only B, because it is shorter? Or both A and B, to make your code more robust?

[Yaël Dillies]

I personally reduce the imports because having reduced imports means it's easier to understand your position in the import tree and perform other algorithms, like looking at all the files that import one you're editing to see what breaks.

[Alex J. Best]

This has been a topic of some discussion in the past. I don't think there is a real consensus, of course most files in mathlib transitively import hundreds of others, and nobody wants to list them all. But some people think that minimizing the set of transitive imports makes the intended background material less clear, and may make splitting / refactoring files harder.
So it's basically up to individual file authors what to do for each file, but PRs changing this on many files will probably generate a lot of debate :grinning:

[Alex J. Best]

The leanproject reduce-imports command can tell you about these transitive imports btw, which is useful when you have a file you know has too many imports at the top.

[Martin Dvořák]

Alex J. Best said:

most files in mathlib transitively import hundreds of others

Do they just import them transitively? Or there examples of a single file that requires hundreds of imports?

[Vincent Beffara]

import_graph.dot.png Just for fun, here is the import graph of the files in mathlib (generated by leanproject import_graph), there does not seem to be vertices with that huge degree.

[Vincent Beffara]

import_graph.clean.dot.png And here is the same graph with redundant imports removed everywhere for comparison.

[Vincent Beffara]

It does not look that different except in the top part where basic things like tactic.basic and data.set live

[Eric Wieser]

Or if you like your hairy messes slightly more colorful, https://eric-wieser.github.io/mathlib-import-graph/

[Martin Dvořák]

How can I add dot.exe to the path so that leanproject will find it?

$ leanproject import-graph
[WinError 2] "dot" not found in path.

I am on Windows 10 and Git bash is open.

[Alex J. Best]

Martin Dvořák said:

Alex J. Best said:

most files in mathlib transitively import hundreds of others

Do they just import them transitively? Or there examples of a single file that requires hundreds of imports?

The only files with really a lot of imports I can think of are catchall imports, like tactic, even some of those will be transitive though. Almost all files have < 10 maximal imports, and most have <=3.

[Alex J. Best]

Do you have graphviz installed? https://graphviz.org/download/#windows

[Martin Dvořák]

Alex J. Best said:

Do you have graphviz installed? https://graphviz.org/download/#windows

I am not sure what "installed" means. I run it from the graphviz folder on my command line (the Windows one).