Zulip Chat Archive

Stream: general

Topic: Diagnosing cyclic imports


view this post on Zulip Eric Wieser (Nov 12 2020 at 11:48):

Is there a tool that will show me the full import cycle / graph?

view this post on Zulip Eric Wieser (Nov 12 2020 at 11:50):

Ah, found leanproject import-graph, which seems to run quite slowly on mathlib

view this post on Zulip Kevin Lacker (Nov 12 2020 at 16:34):

i found grep to be the most useful tool here (or the similar ack)

view this post on Zulip Eric Wieser (Dec 02 2020 at 18:58):

Running into cyclic import issues again in https://github.com/leanprover-community/mathlib/pull/5187 :(

view this post on Zulip Eric Wieser (Dec 02 2020 at 19:14):

It would be really handy if lean could print the full cycle when this happens

view this post on Zulip Eric Wieser (Dec 02 2020 at 19:18):

I get the feeling mathlibtools.leanproject import-graph doesn't work when cyclic imports are present either

view this post on Zulip Eric Wieser (Dec 02 2020 at 19:36):

For some reason even if I revert to a working build and run py -3.8 -m mathlibtools.leanproject import-graph --to data.fintype.basic bad.graphml, I get a file with a single node in it

view this post on Zulip Johan Commelin (Dec 02 2020 at 19:46):

Eric Wieser said:

It would be really handy if lean could print the full cycle when this happens

note that tsort will print cycles. So if you use the bash functions that I posted last time, it might be easy to get the full cycle.

view this post on Zulip Eric Wieser (Dec 02 2020 at 19:55):

Eric Wieser said:

For some reason even if I revert to a working build and run py -3.8 -m mathlibtools.leanproject import-graph --to data.fintype.basic bad.graphml, I get a file with a single node in it

I just tried this again from python - the exception on these lines is being thrown byPath(r"C:/projects/mathlib/src").relative_to("src"). I think this is a mathlibtools bug, although perhaps I have an outdated version

view this post on Zulip Eric Wieser (Dec 02 2020 at 20:00):

Updated to mathlibtools == 1.0.0, but still have the problem. Can someone check if import-graph works for them?

view this post on Zulip Eric Wieser (Dec 03 2020 at 11:16):

leanprover-community/mathlib-tools#88 fixes it for me. cc @Patrick Massot, since you just looked at another mathlibtools thread.

view this post on Zulip Patrick Massot (Dec 03 2020 at 11:46):

Thanks!


Last updated: May 08 2021 at 09:11 UTC