Zulip Chat Archive

Stream: general

Topic: import graph


view this post on Zulip Kenny Lau (Dec 19 2018 at 08:46):

could someone kindly create a graph of imports?

view this post on Zulip Kenny Lau (May 28 2020 at 07:55):

do we have an import graph online?

view this post on Zulip Johan Commelin (May 28 2020 at 07:59):

Not yet, I think. It's WIP

view this post on Zulip Johan Commelin (May 28 2020 at 07:59):

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

view this post on Zulip Kenny Lau (May 28 2020 at 08:03):

what do you mean?

view this post on Zulip Johan Commelin (May 28 2020 at 08:04):

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

view this post on Zulip Johan Commelin (May 28 2020 at 08:04):

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

view this post on Zulip 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"
}

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:08):

Where does the code live for leanproject import-graph?

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:09):

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

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:10):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:11):

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

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:11):

Yeah, thanks for the above

view this post on Zulip Johan Commelin (Nov 23 2020 at 10:12):

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

view this post on Zulip Johan Commelin (Nov 23 2020 at 10:12):

I've never studied graph rendering algorithms

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:12):

.dot is a text format

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:12):

I'm not asking it to render the dot

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:12):

Just write it

view this post on Zulip Johan Commelin (Nov 23 2020 at 10:12):

list_deps | wc -l
2779

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:13):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 23 2020 at 10:13):

Anyway, feel free to improve those bash functions

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:14):

Hence the request for the source

view this post on Zulip Johan Commelin (Nov 23 2020 at 10:14):

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

view this post on Zulip Eric Wieser (Nov 23 2020 at 10:14):

Found: https://github.com/leanprover-community/mathlib-tools/blob/ae9119ced054eb6bec43893b73f832268e495747/mathlibtools/lib.py#L660-L681

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Nov 23 2020 at 12:28):

That might help with discovering related lemmas

view this post on Zulip 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.

view this post on Zulip 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?

Done in leanprover-community/doc-gen#103

view this post on Zulip Eric Wieser (Nov 30 2020 at 16:23):

image.png

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

view this post on Zulip Mario Carneiro (Nov 30 2020 at 16:24):

bit of a funny name

view this post on Zulip Kevin Buzzard (Nov 30 2020 at 16:24):

good name for a band.

view this post on Zulip 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