Mathlib import graph missing edge

Stream: new members

[Snir Broshi]

I downloaded Mathlib's latest import graph from the latest CI build, and I noticed it's missing the edge

"Mathlib.RingTheory.SimpleRing.Basic" -> "Mathlib.RingTheory.Localization.FractionRing";

even though FractionRing does import SimpleRing.Basic on line 12.

I haven't checked for any other missing edges, just ran into this one.
Is this intended (maybe it only lists minimal imports in some sense) or is this a bug?

[Lua Viana Reis]

I think by default it removes transitively redundant edges, see the CLI flag:

https://github.com/leanprover-community/import-graph/blob/451499ea6e97cee4c8979b507a9af5581a849161/Main.lean#L19

[Lua Viana Reis]

running lake exe graph --show-transitive would show all edges

[Snir Broshi]

Nice, that explains it

[Snir Broshi]

I prefer turning this flag on in Mathlib's CI, or at least generate both versions.
I find the full version useful to find common ancestors, for placing theorems which depend on multiple files.
Does anyone have any opinion on the matter?

[Damiano Testa]

Doesn't #find_home help with finding common ancestors?

[Snir Broshi]

I needed to find a file which imports both A and B, and is imported by C.
idk how to use #find_home, can it help with such constraints?

[Damiano Testa]

Slightly artificially: you could create a declaration that is the conjunction of two results from A and B inside C and then ask find home.

[Snir Broshi]

Wow that sounds very useful, I'll try it
I still would like to have the exact graph for more complex analysis, though I don't have a specific use case in mind (that isn't covered by find_home)

[Julian Berman]

I think I added the import-graph artifact upload (which was previously just being built and then not persisted) not too long ago and that probably there aren't a ton of "real" users of the one uploaded during CI. A PR adding the other version I suspect wouldn't be too controversial to merge unless it's gigantic relative to the non-transitive version.

[Julian Berman]

It'd be nice to only generate the non-transitive version and then generate the other one from it (or generate both at once) rather than needing to parse things twice but probably running import-graph isn't a huge amount of time relative to the rest of the CI job.

[Snir Broshi]

How about just having the non-transitive version?

[Damiano Testa]

Mathlib has 7k files, so at most 25mil edges. Storing the transitive graph could occupy the order of 1Gb of space, right? Do you know how much the "slim" one occupies?

[Snir Broshi]

The current one zipped is 270kb

[Damiano Testa]

Ok, I'm not sure how much zipping reduced, but I'm guessing that it is not 3 orders of magnitude, right?

[Damiano Testa]

Anyway, if you could compute the two locally and the sizes are comparable within one or two orders of magnitude, I'd imagine it is not a big deal to have both.

[Damiano Testa]

The cache is various gigabytes, so storing a few extra Mbs won't be a problem

[Snir Broshi]

Damiano Testa said:

Ok, I'm not sure how much zipping reduced, but I'm guessing that it is not 3 orders of magnitude, right?

2mb uncompressed

[Snir Broshi]

Yeah it's less the file size I'm worried about, but CI time

[Damiano Testa]

How much longer to compute the full graph?

[Damiano Testa]

Keeping in mind that the computation of the "big" one from the "small" one could be done locally, and not burden all CI runs with it, I'd be more cautious about that.

[Snir Broshi]

Damiano Testa said:

Keeping in mind that the computation of the "big" one from the "small" one could be done locally, and not burden all CI runs with it, I'd be more cautious about that.

I'm pretty sure it can't be done at all, the reduction is lossy. Only the other direction is possible.

[Damiano Testa]

You can certainly compute the transitive closure.

[Damiano Testa]

What you may not be able to recover is if a file contains a redundant import that gets pruned, but you would not be able to recover that from either the small nor the big version.

[Damiano Testa]

Ideally this should happen very rarely, though, since shake tries to trim imports.

[Snir Broshi]

Damiano Testa said:

You can certainly compute the transitive closure.

A transitive closure is not the inverse of a transitive reduction.
Both operations are lossy.

[Aaron Liu]

I think they for a galois connection between directed trees and irreflexive transitive relations

[Snir Broshi]

Stats based on my laptop:
Full graph - avg 5s to generate, 2.5 MiB, 309 KiB zipped
Reduced graph - avg 10s to generate, 2.0 MiB, 249 KiB zipped

So I think I'll open a PR to add the full graph as an artifact.

[Kim Morrison]

What? Why? I don't understand the motivation here.

[Snir Broshi]

Kim Morrison said:

What? Why? I don't understand the motivation here.

Having the import graph (and not just a transitive reduction of it) can be helpful to do various things.
This thread has a few examples: #new members > Exploring Mathlib

My favorite is that PhysLean have a web version of lake exe graph --from X --to Y: https://physlean.com/Dependencies.html?sources=PhysLean.SpaceAndTime.SpaceTime.Basic,PhysLean.Mathematics.List.InsertIdx,PhysLean.Mathematics.Fin,PhysLean.QFT.PerturbationTheory.CreateAnnihilate&targets=PhysLean.QFT.PerturbationTheory.WickAlgebra.WicksTheorem
I don't know it if uses the transitive reduction or not, but I find it helpful to see the exact import graph.

If my opinion isn't popular then I can generate it locally instead of opening a PR, I didn't know it was that fast to generate.