Zulip Chat Archive

Stream: mathlib4

Topic: Reducing imports to Algebra.CharP.Basic

Yaël Dillies (May 06 2024 at 14:35):

One apparently needs a huge 935 files mess to get to Algebra.CharP.Basic. Anyone up for a challenge? :wink:

Ruben Van de Velde (May 06 2024 at 14:35):

Maybe, but I think I still have some open PRs to split files. Up for a review? :)

Yaël Dillies (May 06 2024 at 14:36):

Dump the PR numbers here. I might have a look during my breaks

Yaël Dillies (May 06 2024 at 14:37):

I should also point out that #11855, #11863, #11986 are relevant here

Ruben Van de Velde (May 06 2024 at 14:54):

https://github.com/leanprover-community/mathlib4/pull/12457 https://github.com/leanprover-community/mathlib4/pull/12493

Ruben Van de Velde (May 06 2024 at 14:54):

I'll look at 11986 later

Yaël Dillies (May 06 2024 at 14:56):

I'm performing a first split of Algebra.CharP.Basic right now

Yaël Dillies (May 06 2024 at 15:13):

#12710

Ruben Van de Velde (May 07 2024 at 15:16):

How do we have a file Group.Defs that defines Group after 1200 lines

Yaël Dillies (May 07 2024 at 15:18):

  1. We don't want to separate out semigroups, monoids, etc
  2. We could move all the defs up and the basic lemmas afterwards, but it's quite impractical due to default fields
  3. The basic lemmas really need to be here as they are needed for forgetful inheritance instances in otherwise mutually cross unimportable files

Johan Commelin (May 07 2024 at 15:20):

I think we should just separate out those other defs

Yaël Dillies (May 07 2024 at 15:21):

By having an Algebra.Monoid folder? :scream:

Yaël Dillies (May 07 2024 at 15:22):

Honestly this is bordering overoptimisation. Algebra.Group.Defs is really fast and has basically no imports.

Eric Rodriguez (May 07 2024 at 15:22):

Files are cheap

Yaël Dillies (May 07 2024 at 15:22):

Nono, here they are really not cheap

Yaël Dillies (May 07 2024 at 15:23):

... because that means separating out a bunch of other downstream files, with lemmas that do not clearly belong to one or the other. And now you also have to think about Units, whose group structure we want to state early on, even though we talk about units of monoids...

Yaël Dillies (May 07 2024 at 15:24):

There are many better fights to take up than trying to reorder Algebra.Group.Defs

Yaël Dillies (May 07 2024 at 15:24):

... eg the titular Algebra.CharP.Basic

Ruben Van de Velde (May 07 2024 at 15:24):

Not necessarily suggesting anything, just surprised

Yaël Dillies (May 07 2024 at 15:25):

It's less surprising once you have needed to tweak the very bottom of the algebraic hierarchy, as I did to define docs#DivisionMonoid

Last updated: May 02 2025 at 03:31 UTC