lake exe graph --from Mathlib.GroupTheory.Perm.Cycle.Factors

Stream: mathlib4

[Kim Morrison]

Today's unreasonable looking import chain:

lake exe graph --from Mathlib.GroupTheory.Perm.Cycle.Factors --to Mathlib.RingTheory.TensorProduct.Basic cyclefactors.png

cyclefactors.png

Anyone feel like cutting that one?

[Yaël Dillies]

Let's have a look

[Johan Commelin]

In fact, if you drop the --to .. flag, you get a graph with 1008 nodes, of which 801 are gray! :open_mouth:

[Yaël Dillies]

Actually, LinearAlgebra.FiniteDimensional.Defs is basically deprecated since docs#FiniteDimensional has been made an abbrev of docs#Module.Finite, so the correct thing to do here is to cut theLinearAlgebra.FiniteDimensional.Defs → RingTheory.TensorProduct.Basic import, which was only needed for a deprecated lemma!

[Yaël Dillies]

PR up at #16468. Definitely easier than I thought it would be :sweat_smile:

[Johan Commelin]

A back-of-the-bash-script calculation shows that this reduces the number of gray nodes downstream from ~80% to ~76%.

[Johan Commelin]

Checking grayfitti for filter: Data
Number of files: 538

Grayfitti: Mathlib.CategoryTheory.GlueData 83%
Grayfitti: Mathlib.Data.Analysis.Filter 86%
Grayfitti: Mathlib.Data.Analysis.Topology 85%
Grayfitti: Mathlib.Data.Array.Defs 88%
Grayfitti: Mathlib.Data.Array.ExtractLemmas 88%
Grayfitti: Mathlib.Data.Array.Lemmas 100%
Grayfitti: Mathlib.Data.BitVec 88%
Grayfitti: Mathlib.Data.Bool.AllAny 90%
Grayfitti: Mathlib.Data.Bool.Basic 84%
Grayfitti: Mathlib.Data.Bool.Count 86%
Grayfitti: Mathlib.Data.Bool.Set 82%
Grayfitti: Mathlib.Data.Bracket 90%
Grayfitti: Mathlib.Data.Bundle 93%
Grayfitti: Mathlib.Data.ByteArray 88%
Grayfitti: Mathlib.Data.Char 94%
Grayfitti: Mathlib.Data.Complex.Abs 71%
Grayfitti: Mathlib.Data.Complex.Basic 67%
Grayfitti: Mathlib.Data.Complex.BigOperators 75%
Grayfitti: Mathlib.Data.Complex.Cardinality 65%
Grayfitti: Mathlib.Data.Complex.Determinant 65%

[Johan Commelin]

It takes about 20~30s per file, on my machine

[Johan Commelin]

I pushed the script to branch#jmc-grayfitti

[Johan Commelin]

It is probably a lot more efficient to do this in one go for an entire import tree. But I just wanted to get some first stats.

[Johan Commelin]

Looks like many import graphs in Mathlib/Data have 60~90% of their nodes colored gray.

[Yaël Dillies]

Things like Data.Bundle or Data.Char I have never even heard of

[Yaël Dillies]

Note however that those things might be needed for tactics, and that's a valid use case which you would accidentally flag

[Johan Commelin]

Yes, true. This can definitely use some tweaking

[Yaël Dillies]

Wait, Data.Bundle is about fiber bundles?! Why is it under Data?

[Yaël Dillies]

I am really confused where Grayfitti: Mathlib.Data.Char 94% comes from given that the only file that imports it is Data.String.Basic (and that one isn't imported anywhere. That still wouldn't explain it, but are you making sure not to count Mathlib.lean in your calculations?

[Johan Commelin]

I am taking the xdot_json file produced by lake exe graph and counting the percentage of e0e0e0 strings compared to Mathlib strings in that file.

[Johan Commelin]

I admit this is maybe not the most robust way of measuring...

[Johan Commelin]

Yaël Dillies said:

Wait, Data.Bundle is about fiber bundles?! Why is it under Data?

Probably for the same reason that Complex.Exponential is under Data?

[Yaël Dillies]

Johan Commelin said:

I am taking the xdot_json file produced by lake exe graph and counting the percentage of e0e0e0 strings compared to Mathlib strings in that file.

For Data.Char, I would expect either 0% or 50%, as explained above, not 94%. So I think something is going wrong but I'm not sure what

[Patrick Massot]

Let me say once a again that I think a lot of things in Data make no sense in this place and should move to another folder.

[Jon Eugster]

Johan Commelin said:

In fact, if you drop the --to .. flag, you get a graph with 1008 nodes, of which 801 are gray! :open_mouth:

Is that true? I thought without a --to flag you should get no grey nodes at all.

[Jon Eugster]

(deleted)

[Johan Commelin]

aah, I guess I was dropping --from :see_no_evil: