Diagnosing cyclic imports

Stream: general

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Lacker]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

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.

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Patrick Massot]

Thanks!

[Bolton Bailey]

Hey, I'm also wanting lean to show me where the cycle is that I've introduced. Is there a good way of doing this / where can I get @Johan Commelin 's bash functions that make this easier?

[Yaël Dillies]

Doing it by hand is usually not too hard if the files concerned do not have transitive imports. A rough knowledge of the library's organisation also helps.

[Bolton Bailey]

Yeah, ok, after focusing and clicking for about a minute I found the cycle, thanks for the advice.

[Bolton Bailey]

It is true that you sort of have to have a working knowledge of how imports in mathlib tend to work though, so I would support the error message printing the cycle.

[Yaël Dillies]

Yeah absolutely! Would be a great addition.

[Bolton Bailey]

Hehe, I am now trying to reconstruct what I did to find the cycle and I can't find it.

[Yaël Dillies]

Importing wrongly once will likely create many cycles, so it's probably hard to find the "meaningful" one.

[Bolton Bailey]

Ok, found it again, crisis averted