Why is CharP.Two so heavy?

Stream: general

[Violeta Hernández]

The file https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/CharP/Two.html has more than 1,000 imports. Which I find quite amazing, considering its lemmas are all quite basic corollaries of characteristic two rings. Where are these imports coming from? Is it literally just the docs#orderOf import?

[Edward van de Meent]

Violeta Hernández said:

has more than 1,000 imports

does this mean "directly imports", "is directly imported by", "transitively imports" or "is transitively imported by" more than 1000 files?

[Violeta Hernández]

All I know is that it's been building for like 20 minutes
imagen.png

[Eric Wieser]

That number includes batteries too, probably

[Violeta Hernández]

I still think this number is way too high for the material it actually contains. I'd expect something closer to half.

[Violeta Hernández]

also, the actual number is closer to 1200...

[Eric Wieser]

Maybe https://leanprover-community.github.io/mathlib4_docs/mathlib.html?highlight=Mathlib.Algebra.CharP.Two is helpful

[Eric Wieser]

Ah, the highlight is the opposite of what you want

[Ruben Van de Velde]

Does the import graph script still work?

[Alex Meiburg]

Yeah, I wonder how much of that can be explained by import Batteries; import Aesop; import Mathlib.Tactic.Linarith; import Mathlib.Tactic.Ring

[Ruben Van de Velde]

Yeah, those all seem somewhat heavy

[Thomas Browning]

I think the OrderOfElement import is the big one, since that file is designed to be a one-stop shop for the theory of orders of elements in groups, which means that it pulls in all of the subgroup theory (via GroupTheory.Index) among other things

[Violeta Hernández]

Would it make sense to split OrderOfElement into a Defs file and one with the rest of the API?

[Violeta Hernández]

And then CharP.Two hopefully only needs the former

[Eric Wieser]

Is this heavy dependency causing a problem?

[Eric Wieser]

Generally leaf files (like CharTwo) have much heavier dependencies than trunk files, because there's a tradeoff to be made between small dependencies and small number of files

[Violeta Hernández]

It's not a problem, but it is annoying. I use CharTwo somewhat heavily in the CGT repo and it's one of the heaviest imports in the files that use it.

[Kevin Buzzard]

I don't understand why that is annoying. What problems is it causing you?

[Violeta Hernández]

It means that if I modify anything I have to wait for half an hour for everything to rebuild.

[Kevin Buzzard]

I'm still confused. I use a bazillion algebra files with thousands of transitive imports in FLT and I have never once found this fact annoying in any way. I modify FLT code all the time and I don't have to wait at all. What exactly are you modifying?

[Violeta Hernández]

Well, a few hours ago I added a few new lemmas to the file, but my PR also added a new lemma in a very early file, which meant I had to compile most of these 1200 imports from scratch.

[Kevin Buzzard]

Wait -- you are modifying mathlib files within the CGT repo?

[Kevin Buzzard]

Why not just put your changes in the Mathlib or ForMathlib or whatever you're calling it directory in the CGT repo and then PR them?

[Kevin Buzzard]

then when the PR is merged you just bump and delete the files and get cache.

[Violeta Hernández]

Sorry, let me word things better. It's annoying modifying that file when making Mathlib PRs because there's a lot to build. And I've had to modify that file a few times in the past because it's imported in the CGT repo.

[Bryan Wang]

I encountered this problem where in a mathlib branch (in preparation for a mathlib PR) I modified two files A and B, where B transitively imports A but along a super long chain. The build of file B takes forever and I wondered if there is a smarter way around this (other than splitting into two PRs)

[Kevin Buzzard]

Surely you don't mean "it's annoying modifying that leaf file", you mean "it's annoying modifying a very early file and that leaf file at the same time", but this is a special case of "it's annoying modifying a very early file" because this breaks not just your leaf file but pretty much everything.

Does the module system not help here? Is there some clever public/private change which would make your life easier?

[Snir Broshi]

btw it has 948 imports in Mathlib (imports.txt)

[Kim Morrison]

@Violeta Hernández, do you know how to use lake exe graph --from ... --to ... out.pdf? I find this quite useful understand the import tangles in Mathlib.

[Bryan Wang]

Kevin Buzzard said:

, but this is a special case of "it's annoying modifying a very early file" because this breaks not just your leaf file but pretty much everything.

If I modify only a very early file in mathlib, I don't feel the pain as much because the slowness happens in github CI, and not on my machine :stuck_out_tongue_closed_eyes:

[Violeta Hernández]

Maybe there's a separate question I should be asking. Isn't minimizing imports of any given file generally a good thing? If there was some simple tweak I could do which halved the amount of imports of this file, would it not be a good change?

[Yaël Dillies]

It would be a good change if it didn't involve an unnatural split of the file

[Violeta Hernández]

Then I'll try and if I can achieve that I'll PR it

[Yuyang Zhao]

#34663 moves the lemmas about docs#orderOf to GroupTheory.OrderOfElement and minimizes dependencies on Algebra.CharP.Two, so that reversing the import direction adds only one dependency to GroupTheory.OrderOfElement.

[Jon Eugster]

Ruben Van de Velde said:

Does the import graph script still work?

(I'd hope so! Report issues if there are any doubts in it's functionality :wink: )