## Stream: general

### Topic: import graph

#### Kenny Lau (Dec 19 2018 at 08:46):

could someone kindly create a graph of imports?

#### Kenny Lau (May 28 2020 at 07:55):

do we have an import graph online?

#### Johan Commelin (May 28 2020 at 07:59):

Not yet, I think. It's WIP

#### Johan Commelin (May 28 2020 at 07:59):

Also... now you have to update the title and first post of your PR :rofl:

#### Kenny Lau (May 28 2020 at 08:03):

what do you mean?

#### Johan Commelin (May 28 2020 at 08:04):

Well... you're now attacking nonzero_divisors as well, right?

#### Johan Commelin (May 28 2020 at 08:04):

It's less drastic, but it would be nice to mention it.

#### Johan Commelin (Nov 23 2020 at 10:08):

@Eric Wieser Here are some bash functions that will build the import graph for you within seconds:

function file_to_import {
sed -e 's/src\///;s/.lean//;s/\//./g'
}

function import_to_file {
sed -e 's/[.]/\//g;s/.*/src\/&.lean/'
}

function list_deps {
find src/ -name '*.lean' \
| xargs grep "^import " \
| sed -e 's/src\///;s/.lean:import//;s/\//./g;s/ --.*//' \
| grep -v "tactic.norm_num data.real.basic" \
| grep -v "tactic.find tactic.find"
}


#### Eric Wieser (Nov 23 2020 at 10:08):

Where does the code live for leanproject import-graph?

#### Johan Commelin (Nov 23 2020 at 10:09):

Output is in tsort format, in other words: one edge per line

A B
C D
E F
A D
A F


etc...

#### Eric Wieser (Nov 23 2020 at 10:09):

Searching mathlib-tools for import-graph finds only one match in a changelog

#### Eric Wieser (Nov 23 2020 at 10:10):

ImportGraph finds a slightly better match, but only an unused definition.

#### Johan Commelin (Nov 23 2020 at 10:11):

@Eric Wieser it really depends on what you want to do. I guess the rendering is what is taking a long time.

#### Johan Commelin (Nov 23 2020 at 10:11):

But if you just want the data, I guess the functions I gave above are a good first start.

#### Eric Wieser (Nov 23 2020 at 10:11):

The default is .dot though right, which should be trivial to render

#### Eric Wieser (Nov 23 2020 at 10:11):

Yeah, thanks for the above

#### Johan Commelin (Nov 23 2020 at 10:12):

Not sure if rendering dot files the size of mathlibs import graph is trivial.

#### Johan Commelin (Nov 23 2020 at 10:12):

I've never studied graph rendering algorithms

#### Eric Wieser (Nov 23 2020 at 10:12):

.dot is a text format

#### Eric Wieser (Nov 23 2020 at 10:12):

I'm not asking it to render the dot

Just write it

#### Johan Commelin (Nov 23 2020 at 10:12):

list_deps | wc -l
2779


#### Eric Wieser (Nov 23 2020 at 10:13):

Although I suppose it might be running the layout engine in advance.

#### Johan Commelin (Nov 23 2020 at 10:13):

Ooh, so you just want a -> between the source and target, basically. And then a digraph FOOBAR { at the start of the file, and a } at the end.

#### Johan Commelin (Nov 23 2020 at 10:13):

Anyway, feel free to improve those bash functions

#### Eric Wieser (Nov 23 2020 at 10:13):

Not sure I'd go as far as saying that's what I want, but that's what I imagine import-graph already does

#### Eric Wieser (Nov 23 2020 at 10:14):

I just don't know what it actually does because I've never managed to invoke it successfully

#### Eric Wieser (Nov 23 2020 at 10:14):

Hence the request for the source

#### Johan Commelin (Nov 23 2020 at 10:14):

leanproject is producing a dot file with layout instructions, not just the raw graph data.

#### Patrick Massot (Nov 23 2020 at 12:23):

Eric Wieser said:

Searching mathlib-tools for import-graph finds only one match in a changelog

What about actually reading that page instead of complaining about GitHub? It says it found two relevant commits.

#### Patrick Massot (Nov 23 2020 at 12:24):

You'll then see that this command runs lean --deps to get reliable import information that regex will never give you. However we are pretty strict in mathlib about import lines formatting so ideally the regex based version should almost give the same information (much much faster).

#### Patrick Massot (Nov 23 2020 at 12:25):

Of course running the full thing on uncompiled mathlib is a very bad idea. But on a compiled mathlib it should take less than 30 seconds.

#### Eric Wieser (Nov 23 2020 at 12:28):

Yeah, the key takeaway here was that .dot output is also doing graph layout, which I wasn't expecting. Using graphml output was much faster

#### Eric Wieser (Nov 23 2020 at 12:28):

Perhaps a compromise regarding docs would be to add an "imports" and "imported by" section to each page?

#### Eric Wieser (Nov 23 2020 at 12:28):

That might help with discovering related lemmas

#### Eric Wieser (Nov 23 2020 at 12:29):

I'll have a go at that once a decision is made about leanprover-community/doc-gen#102, since they'll interact quite a bit and the ImportName object there will help resolve the paths.

#### Eric Wieser (Nov 30 2020 at 12:46):

Eric Wieser said:

Perhaps a compromise regarding docs would be to add an "imports" and "imported by" section to each page?

#### Eric Wieser (Nov 30 2020 at 16:23):

With thanks to @Gabriel Ebner for putting it somewhere sensible on the page

#### Mario Carneiro (Nov 30 2020 at 16:24):

bit of a funny name

#### Kevin Buzzard (Nov 30 2020 at 16:24):

good name for a band.

#### Eric Wieser (Dec 01 2020 at 11:32):

I had a go at building an interactive import graph for my lean project:

https://observablehq.com/@eric-wieser/lean-ga-imports

I don't know how well this would perform with a full mathlib graph...

Last updated: May 14 2021 at 00:42 UTC