Comm vs non-Comm instance design

Stream: mathlib4

[Matthew Ballard]

Kevin Buzzard said:

IMG_20250413_222335365_HDR.jpg

I think that's what mathlib looks like currently, regarding {NonUnital/unital}{non-comm/Comm}{no norm/Seminorm/Norm}ed rings (so non-unital rings in the bottom left up to normed commutative rings in the top right, with seminormed rings in the middle). A red X means that the instance is present but has priority 100. The slightly curvy lines are NonUnitalNormedCommRing.toNonUnitalCommRing (i.e. skip the non-unital seminormed commutative ring) and NormedCommRing.toCommRing. A notable absentee is Seminormed Ring.toRing which presumably has default prio and which Matt explicitly flagged as perhaps causing a problem in the PR (note that SeminormedCommRing.toCommRing has prio 100). I don't know how to find the priority of SeminormedRing.toRing, I guess it could have prio lowered elsewhere.

What should the logic of the diagram be? Are we being inconsistent and paying for it now?

Is the picture supposed to be saying "Here are 12 classes but we really really really don't want you to deduce any of them from any of the others, except that you are allowed to deduce X from CommX"? Because that it what it says right now. It seems like a very weird set-up to me.

I tried to think about this in two ways:

1. Avoid the CommX.toX instances as much as possible by lowering the priorities #24140
2. Jump at the first opportunity to the Comm level and stay there by raising the priorities (WIP to build)

I am not sure of which is better overall for performance.

1) has advantage of avoiding failing searches and not straying into Comm classes if needed. The disadvantage is that you in general need to unify against longer chains of instances, eg CommRing.toRing Ring.toSemiring vs CommRing.toCommSemiring CommSemiring.toSemiring when you are using a result that takes a [CommSemiring R]as a parameter for something with [CommRing R] as a parameter that needs a Semiring R.

2) has advantage that the jump to the Comm class occurs at the first opportunity avoiding the unifications but the disadvantage of possibly more failing searches for Comm instances on non-Comm things.

[Matthew Ballard]

The results for 1 are in and not terrible.

  Benchmark                                              Metric          Change
  =============================================================================
+ build                                                  instructions     -0.8%
+ build                                                  type checking    -5.7%
- ~Mathlib.Algebra.Module.FinitePresentation             instructions     14.9%
+ ~Mathlib.AlgebraicGeometry.AffineSpace                 instructions     -9.7%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Affine        instructions     -7.5%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Group         instructions    -10.7%
+ ~Mathlib.Analysis.CStarAlgebra.lpSpace                 instructions    -38.8%
+ ~Mathlib.CategoryTheory.Preadditive.Mat                instructions    -13.8%
+ ~Mathlib.FieldTheory.RatFunc.Basic                     instructions     -5.2%
- ~Mathlib.Geometry.Euclidean.Basic                      instructions     23.1%
- ~Mathlib.Geometry.Euclidean.Circumcenter               instructions     15.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic           instructions    -26.9%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even            instructions    -11.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv       instructions    -17.6%
+ ~Mathlib.NumberTheory.KummerDedekind                   instructions    -19.0%
+ ~Mathlib.RingTheory.AdjoinRoot                         instructions    -10.8%
+ ~Mathlib.RingTheory.Algebraic.Integral                 instructions    -47.5%
+ ~Mathlib.RingTheory.ClassGroup                         instructions    -26.3%
- ~Mathlib.RingTheory.CotangentLocalizationAway          instructions     15.6%
+ ~Mathlib.RingTheory.DedekindDomain.Different           instructions    -23.4%
+ ~Mathlib.RingTheory.Extension                          instructions     -6.9%
- ~Mathlib.RingTheory.FinitePresentation                 instructions     36.2%
+ ~Mathlib.RingTheory.FiniteStability                    instructions    -28.5%
- ~Mathlib.RingTheory.Generators                         instructions     36.7%
+ ~Mathlib.RingTheory.Ideal.Norm.AbsNorm                 instructions    -36.5%
+ ~Mathlib.RingTheory.Ideal.Norm.RelNorm                 instructions    -18.5%
+ ~Mathlib.RingTheory.Ideal.Quotient.Operations          instructions     -8.7%
+ ~Mathlib.RingTheory.IntegralClosure.IntegralRestrict   instructions    -19.2%
+ ~Mathlib.RingTheory.Jacobson.Ring                      instructions    -23.0%
+ ~Mathlib.RingTheory.Kaehler.Basic                      instructions     -8.6%
+ ~Mathlib.RingTheory.Kaehler.JacobiZariski              instructions    -21.6%
+ ~Mathlib.RingTheory.Kaehler.TensorProduct              instructions     -8.1%
+ ~Mathlib.RingTheory.LaurentSeries                      instructions    -11.1%
- ~Mathlib.RingTheory.NoetherNormalization               instructions     37.4%
+ ~Mathlib.RingTheory.Polynomial.Quotient                instructions    -27.2%
+ ~Mathlib.RingTheory.PowerSeries.Basic                  instructions    -31.5%
- ~Mathlib.RingTheory.Presentation                       instructions     26.6%
+ ~Mathlib.RingTheory.WittVector.Isocrystal              instructions    -24.5%

[Matthew Ballard]

Note that Mathlib.RingTheory.Kaehler.JacobiZariski is particularly happy

[Xavier Roblot]

It's still more green than red, I think, and it would probably help to speed up #24108

[Matthew Ballard]

I haven't had time to finish the other approach yet and I am not sure when I will find it with finals coming up...

[Matthew Ballard]

branch#mrb/bump_comm_prios_up

[Matthew Ballard]

I took a look after the mild performance hit of #24004 and it was another in this line where Lean needs to unify Comm to non-Comm diamonds over and over again. What makes the most sense to me is making Comm a mixin. If we would could expand [[CommRing R]] to [Ring R] [IsCommMul R] I think we wouldn’t really lose much in terms of usability.

[Andrew Yang]

Does class_abbrevs help here? Or do they cause the same slowdowns?

[Jovan Gerbscheid]

Is there a notation [[...]] for bundling type class assumptions? Or are you suggesting to define this?

[Matthew Ballard]

There is no notation. I don’t what class_abbrev is…

[Jovan Gerbscheid]

Given classes A a and B a, you can use class_abbrev to define a class C a that is equivalent to having A a and B a. This does what you want, but it is horribly inefficient.

This is because it adds instances both from and to C a. Meaning that if you are searchin for an instance of B a, it obtains the subgoal of finding an instance of C a. And then it finds the pair of subgoals A a and B a. And then it starts synthesizing A a, which is completely unrelated to the original goal B a.

[Matthew Ballard]

I think it should just be a macro and its on the user or a linter to make sure there is no doubling up of Mul

[Matthew Ballard]

Where does it live? In core?

[Jovan Gerbscheid]

I agree that there should be a system for introducing multiple type class assumptions with one notation. For example, I'd love to write [[AffineSpace ℝ V P]] instead of [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]. I could even imagine a world where this uses the same [..] brackets as a usual type class assumptions. In that case it wouldn't be a macro, but a built-in feature that acts based on whether the term is a type class or this new thing.

[Matthew Ballard]

I worry about overhead if it is not a macro

[Andrew Yang]

What about variable_alias? I know that the usage of it (and variable?) is banned in mathlib but this seems similar to what you are looking for and can someone remind we why they are banned?

[Kyle Miller]

(I told @Matthew Ballard this in person today, but I'm currently investigating adding binder macros as part of some other adjacent work. Possibly user-definable binder elaborators are on the table too, but I won't promise this.)

[Jovan Gerbscheid]

My idea was to define it as follows. We have a notation like

class_abbrev' AffineSpace (R V P : Type*) :=
  [NormedAddCommGroup V] [InnerProductSpace R V] [MetricSpace P] [NormedAddTorsor V P]

which creates a structure

structure AffineSpace (R V P : Type*) where
  a1 : NormedAddCommGroup V
  a2 : InnerProductSpace R V
  a3 : MetricSpace P
  a4 : NormedAddTorsor V P

Then, when elaborating an instance binder [AffineSpace R V P], in the current implementation, it finds the name of the underlying structure (AffineSpace), and looks it up in the environment to see if it is a class. Then I propose if it is not a class, it looks it up in this class_abbrev' environment extension. When it finds that it is a class abbreviation, it recursively adds all the structure fields as type class hypotheses.

With this design there is no overhead to worry about.

Edit: I guess the constructor and projection functions should be made inaccessible, since the structure is not meant to actually be used.

[Matthew Ballard]

That seems reasonable also

[Kyle Miller]

@Jovan Gerbscheid Take a look at variable_alias, what @Andrew Yang mentioned. It's pretty much the same idea. It's not recursive though.

[Jovan Gerbscheid]

Where can it be found?

[Kyle Miller]

I don't know if there are any mathlib examples except in the tests folder. Here's where it's implemented: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Variable.lean

It's only for variable?

[Andrew Yang]

There are e.g. docs#HilbertSpace that implements variable_alias but as I said it is banned in mathlib somehow.

[Yury G. Kudryashov]

It's banned in Mathlib, because it works with variable?, not variable. I think that we should improve support for variable aliases so that one can write [HilberSpace K V] in variable or theorem assumptions and get the right thing, possibly with slightly different syntax, e.g., [[HilbertSpace K V]].

[Yury G. Kudryashov]

Then we can turn [Comm*] into variable aliases and have 2 separate searches, one in the non-commutative hierarcy, and one for IsMulCommutative.

[Andrew Yang]

Yeah my question is why is variable? banned? Is it just because it is noisy by default or is it a conscious decision?

[Kyle Miller]

(@Yury G. Kudryashov Is this different from what Matt proposed in his first message today in this thread?)

[Jovan Gerbscheid]

I can see why variable? is discouraged: it automatically infers the arguments that it thinks it needs. My suggested system is transparent: it is clear what hypotheses are added. And you have more control over it.

[Kyle Miller]

Are people aware that variable? expands to the full form?

However, even when expanded it still does the expansion to verify that the expanded form is correct. It's like says.

[Yury G. Kudryashov]

Kyle Miller said:

(Yury G. Kudryashov Is this different from what Matt proposed in his first message today in this thread?)

No, it's the same (modulo the question about auto deducing preexisting instances). I'm sorry for answering the last question without reading history. I'm going offline for several hours now, then I'll reread this thread.

[Jovan Gerbscheid]

Kyle Miller said:

Are people aware that variable? expands to the full form?

Oh I see. But I want this feature for readability. I want to reduce the number of characters it takes to read/write e.g. [PID P], instead of [CommRing P] [IsDomain P] [IsPrincipalIdealRing P]

[Sébastien Gouëzel]

There was a recent discussion about this. I sketched a possible design in #mathlib4 > Normed modules @ 💬 which looked reasonable to the participants of the discussion at the time.

[Matthew Ballard]

Yes. I should have referenced this explicitly but assumed everyone remembered.

[Matthew Ballard]

Probably not a good assumption

[Kyle Miller]

@Sébastien Gouëzel Thanks, I just read the thread. The proposed feature sounds like the @[variable_alias] feature for variable?, correct?

There's a performance issue, but it's not the worst. Deciding whether or not to include an instance requires failing instance searches, which tend to be slow since Lean will go to great lengths to find an instance.

[Kyle Miller]

Ah, I misread. Double brackets invokes the variable? behavior. Still, the performance point stands.

[Jovan Gerbscheid]

I think that such a design as in variable?, which automatically decides whether to add an instance, isn't great.

• It adds an overhead for the reader to figure out what hypotheses are added.
• It seems fragile because a theorem could gain an unintended type class assumption because of a change upstream.

[Kyle Miller]

Jovan Gerbscheid said:

Oh I see. But I want this feature for readability. I want to reduce the number of characters it takes to read/write e.g. [PID P], instead of [CommRing P] [IsDomain P] [IsPrincipalIdealRing P]

I have an impression you haven't tried variable?. With

variable? [Module R M]

there is a code action to expanding it to

variable? [Module R M] => [Semiring R] [AddCommMonoid M] [Module R M]

Or, in the tests file,

variable? [VectorSpace R M]

there is a code action expanding it to

variable? [VectorSpace R M] => [Field R] [AddCommGroup M] [Module R M]

I don't think variable? is the full answer, especially if we could get a reasonable [[Module R M]] as an actual binder notation, but I want to understand what your objection is, in case I misunderstood whether you knew what the expansions looked like.

Having the => part is basically for review purposes and for protecting against changes to typeclass hierarchy. It's there for similar reasons to why some people support keeping autoimplicits off in Mathlib even if we have inlay hints for them in our IDEs.

(@Andrew Yang I'm not sure why variable? with a => clause is banned in mathlib. I'm not even sure whether or not it is banned.)

[Jovan Gerbscheid]

Right, in my message I was referring to a design without the =>, which is think is what is being proposed

[Jovan Gerbscheid]

I think my proposed design should allow us to refactor the Comm vs non-Comm instance design without having to touch many of the theorems, or having to worry about whether got the correct hypotheses.

[Sébastien Gouëzel]

To me, an important issue is readability, which is already a little bit problematic in examples like

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]

example : ContMDiffVectorBundle ∞ E (TangentSpace I : M → Type _) I := by infer_instance

Here, the variable is the minimal one to make sense of the statement, and it's already super long. If we decouple algebra from topology, as has been discussed (and is certainly a very good idea if the readability issues are solved), this would become

variable {𝕜 : Type*} [Field 𝕜] [Norm 𝕜] [IsNontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {E : Type*} [AddGroup E] [IsCommAdd E] [Norm E] [IsNormedAddCommGroup E] [IsNormedSpace 𝕜 E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]

example : ContMDiffVectorBundle ∞ E (TangentSpace I : M → Type _) I := by infer_instance

which is even longer. Being able to just have

variable {𝕜 : Type*} {n : WithTop ℕ∞} {E : Type*} [[IsNormedSpace 𝕜 E]]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [[IsManifold I ∞ M]]

would be a tremendous improvement in this respect.

[Kyle Miller]

The only differences @Jovan Gerbscheid between what you're proposing and variable? are:

1. There's a feature to add missing instances on instance synthesis failure. That can be disabled easily enough.
2. Rather than use fields of a structure, it uses parameters of a structure to record @[variable_aliases] (there are some good reasons to do this instead of using fields, beyond just supporting 1, but without 1 the design would probably need to be a bit different).
3. It has a code action to add the expanded form, for review.

[Kyle Miller]

4. This is just for variables rather than binders in declarations. (But until core is extended that's a fundamental limitation.)

[Matthew Ballard]

I thought he wanted it in declarations also misread.

[Kyle Miller]

Me too Matt :-) But for completeness of the list of differences I thought I should include it.

[Jovan Gerbscheid]

5. My proposal doesn't add any new syntax for stating theorems. We can just use the familiar [..] instance binders.

[Kyle Miller]

Noted, though that's not a difference between your proposal and variable?.

[Kyle Miller]

@Sébastien Gouëzel Introducing manifolds is such a chore, and I hope it's not always going to be multiple lines of variable declarations...

When implementing variable? I found that adding the missing instances as new binders didn't always work right. I don't have any examples off-hand, but it was something to do with when you have a list of instance binders, you sort of need to look at the whole list to see what the "right" missing instance binders to add are. (Choices for earlier binders might throw later binders off.)

Some sort of aliasing system to be able to control which missing instances to add would go a long way toward making things usable/maintainable. (Even if it's not based on what's missing, but a simple macro expansion.)

One thought that comes to mind is having a missing instance system that only looks to see which local instances already exist (no global search). A downside is that it might add binders for things like [Field ℝ] just because it's not a local instance. Maybe that's something that can be linted for.

[Jovan Gerbscheid]

Well, variable? .. => .. seems like new syntax needed to understand theorems

[Kyle Miller]

What I'm trying to say @Jovan Gerbscheid is that your proposal is basically explored in variable? already, so I'm not sure what you're objecting to.

[Kyle Miller]

I brought up the specifics of how => worked because it seemed like you were objecting to the fact that variable? had an expansion feature, and it seemed like you thought it meant that you couldn't see the short form anymore.

[Kyle Miller]

(Or, said differently, if there's something different about your proposal and how @[variable_alias] works, I'm interested to hear it. I just find it hard to understand what's different without a careful comparison.)

[Sébastien Gouëzel]

If there is a performance issue with the complicated design where on tries to synthetize the missing instances, I think the more simple-minded approach of just adding the intermediate instances if they are not already present in the context would already be helpful for readability.

I mean, with something like

variable_alias (𝕜 E : Type*) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] NormedVectorSpace

variable {𝕜 E F : Type*} [[NormedVectorSpace 𝕜 E]] [[NormedVectorSpace 𝕜 F]]

then the last variable line would be interpreted as

variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
  [NormedSpace 𝕜 E] [NormedSpace 𝕜 F]

And it's the responsability of the user to make sure there is not already a [NormedField 𝕜] around, because this would give two field structures on 𝕜, in the same way that currently it's the responsability of the user to make sure we don't have [Ring R] [CommRing R].

[Johan Commelin]

@Sébastien Gouëzel Naively, that last line would become

variable {𝕜 E F : Type*}
variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F]

right?
So you do want the system to be responsible for not inserting a second copy of [NontriviallyNormedField 𝕜], is that right?

[Sébastien Gouëzel]

Yes. I wrote "just adding the intermediate instances if they are not already present in the context" precisely for this issue. Just looking whether an instance is already there in this exact form, without launching typeclass inference, should be very cheap and avoid the performance issue @Kyle Miller was afraid of, hopefully.

[Johan Commelin]

Aha, understood. That makes sense.

[Yury G. Kudryashov]

This won't help with [[NormedSpace Real E]]. What about "run typeclass instance with high priority instances only"? Or does it require a fix in the core for priority of extends?

[Sébastien Gouëzel]

Yes, this won't help in some situations. But still it would be helpful in many situations -- for instance if you want to refactor [CommGroup E] to become [Group E] [IsMulComm E], then replacing [CommGroup (.)] with [[CommGroup $1]] throughout the library would be enough.

[Jovan Gerbscheid]

I think that (A) "binding multiple type classes in one go" and (B) "automatically binding missing type classes" are different features that should be independently available. My proposal only does (A). Then if we also want (B), I propose that we use [[..]] notation for it.

@Kyle Miller, the difference between my proposal and variable? is that when declaring a class_abbrev', there is a distinction between parameters and field. For example, a normed vectorspace would be

class_abbrev' NormedVectorSpace
    (𝕜 E : Type*) [NontriviallyNormedField 𝕜] :=
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]

And we can introduce two of them with

variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜]
variable [NormedVectorSpace 𝕜 E] [NormedVectorSpace 𝕜 F]

Or using (B), it would be what @Sébastien Gouëzel wrote:

variable {𝕜 E F : Type*} [[NormedVectorSpace 𝕜 E]] [[NormedVectorSpace 𝕜 F]]

I worry about both the mental and computational overhead that (B) would add. But if we can use (A) without (B), then I have no objection to adding (B). On the other hand I think (B) without (A) is also useful, e.g. writing [[LawfulBEq α]] instead of [BEq α] [LawfulBEq α].

[Jovan Gerbscheid]

Another consideration for my proposal for (A) is whether [NormedVectorSpace 𝕜 E] should actually be expanded into [NormedAddCommGroup E] [NormedSpace 𝕜 E] when elaborating the statement or not. My goal is to improve readability, so it would be beneficial if the type of a theorem about normed vectorspaces contained hypothesis[NormedVectorSpace 𝕜 E] instead of [NormedAddCommGroup E] [NormedSpace 𝕜 E]. This would be useful when hovering over the theorem.

Implementing this would mean that docs#Lean.LocalInstance should be able to contain a structure projection of a free variable, instead of just a free variable. And when adding a variable to the local context, it would add the fields of a class_abbrev as local instances. And the constructor of the class_abbrev' would have to be tagged as the only instance of the class.

At this point this could just be a refactor of class abbrev instead of a separate feature.

[Matthew Ballard]

Returning to the original approach in the thread: #24429 which tries to keep you in the CommX level of the instance graph as long as possible once you start there shows now builds enough for benchmarking

[Matthew Ballard]

  Benchmark                                                                    Metric         Change
  ==================================================================================================
- build                                                                        instructions    1.01%
- ~Mathlib.Algebra.Algebra.Subalgebra.Rank                                     instructions    59.3%
- ~Mathlib.Algebra.DirectSum.Internal                                          instructions    23.8%
+ ~Mathlib.Algebra.Lie.TraceForm                                               instructions    -7.8%
+ ~Mathlib.Algebra.Lie.Weights.Killing                                         instructions    -5.0%
- ~Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic                         instructions    22.8%
- ~Mathlib.Algebra.TrivSqZeroExt                                               instructions    11.8%
+ ~Mathlib.AlgebraicGeometry.AffineSpace                                       instructions    -4.2%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper                         instructions   -21.0%
- ~Mathlib.Analysis.Asymptotics.Defs                                           instructions    15.2%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances        instructions    -5.7%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict         instructions   -19.5%
- ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital           instructions    11.3%
- ~Mathlib.Analysis.CStarAlgebra.GelfandDuality                                instructions    13.8%
- ~Mathlib.Analysis.CStarAlgebra.Matrix                                        instructions    33.5%
- ~Mathlib.Analysis.Complex.UpperHalfPlane.Basic                               instructions   116.1%
- ~Mathlib.Analysis.Convolution                                                instructions     6.9%
- ~Mathlib.Analysis.InnerProductSpace.Adjoint                                  instructions    38.8%
- ~Mathlib.Analysis.InnerProductSpace.Projection                               instructions     7.1%
- ~Mathlib.Analysis.Normed.Field.UnitBall                                      instructions    93.1%
- ~Mathlib.Analysis.Normed.Lp.lpSpace                                          instructions     5.0%
+ ~Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic   instructions    -6.7%
+ ~Mathlib.FieldTheory.CardinalEmb                                             instructions   -14.2%
+ ~Mathlib.FieldTheory.Extension                                               instructions   -23.8%
+ ~Mathlib.FieldTheory.Galois.Infinite                                         instructions   -21.9%
- ~Mathlib.FieldTheory.Galois.Profinite                                        instructions    79.8%
+ ~Mathlib.FieldTheory.IntermediateField.Adjoin.Basic                          instructions   -11.1%
+ ~Mathlib.FieldTheory.IntermediateField.Adjoin.Defs                           instructions   -22.9%
+ ~Mathlib.FieldTheory.IntermediateField.Basic                                 instructions   -29.9%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                            instructions   -28.9%
- ~Mathlib.FieldTheory.KummerExtension                                         instructions    21.8%
+ ~Mathlib.FieldTheory.LinearDisjoint                                          instructions   -13.4%
+ ~Mathlib.FieldTheory.PurelyInseparable.Basic                                 instructions   -29.3%
- ~Mathlib.FieldTheory.RatFunc.Basic                                           instructions     4.6%
+ ~Mathlib.FieldTheory.SeparableDegree                                         instructions   -21.6%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation                   instructions    -6.0%
- ~Mathlib.Geometry.Manifold.ContMDiff.NormedSpace                             instructions    14.8%
- ~Mathlib.Geometry.Manifold.MFDeriv.NormedSpace                               instructions    14.7%
- ~Mathlib.GroupTheory.HNNExtension                                            instructions    19.0%
- ~Mathlib.GroupTheory.SpecificGroups.ZGroup                                   instructions    56.1%
- ~Mathlib.GroupTheory.Sylow                                                   instructions    54.0%
- ~Mathlib.GroupTheory.Transfer                                                instructions    75.2%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                            instructions    20.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                                 instructions   -29.7%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                                  instructions    25.7%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                             instructions    66.2%
- ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                               instructions   149.7%
+ ~Mathlib.LinearAlgebra.Dual.Lemmas                                           instructions    -6.3%
- ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                               instructions    38.1%
- ~Mathlib.LinearAlgebra.ExteriorPower.Basic                                   instructions    12.8%
- ~Mathlib.LinearAlgebra.FreeProduct.Basic                                     instructions    68.9%
- ~Mathlib.LinearAlgebra.RootSystem.Irreducible                                instructions   100.6%
- ~Mathlib.LinearAlgebra.RootSystem.WeylGroup                                  instructions    81.4%
+ ~Mathlib.LinearAlgebra.Semisimple                                            instructions   -26.2%
- ~Mathlib.LinearAlgebra.TensorAlgebra.Grading                                 instructions   210.6%
- ~Mathlib.LinearAlgebra.TensorProduct.Graded.Internal                         instructions     4.8%
- ~Mathlib.LinearAlgebra.TensorProduct.Subalgebra                              instructions    11.2%
- ~Mathlib.MeasureTheory.Group.FundamentalDomain                               instructions    11.0%
- ~Mathlib.MeasureTheory.Measure.Haar.Disintegration                           instructions    62.8%
- ~Mathlib.NumberTheory.ModularForms.SlashActions                              instructions   139.0%
+ ~Mathlib.RingTheory.AdjoinRoot                                               instructions    -8.5%
- ~Mathlib.RingTheory.Algebraic.MvPolynomial                                   instructions    32.1%
- ~Mathlib.RingTheory.AlgebraicIndependent.Basic                               instructions    39.7%
- ~Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis                  instructions    17.2%
+ ~Mathlib.RingTheory.ClassGroup                                               instructions   -10.8%
- ~Mathlib.RingTheory.DedekindDomain.AdicValuation                             instructions    48.9%
+ ~Mathlib.RingTheory.DedekindDomain.Ideal                                     instructions    -6.7%
- ~Mathlib.RingTheory.EssentialFiniteness                                      instructions    36.7%
- ~Mathlib.RingTheory.Filtration                                               instructions    36.3%
- ~Mathlib.RingTheory.FinitePresentation                                       instructions    33.9%
- ~Mathlib.RingTheory.Generators                                               instructions    35.5%
- ~Mathlib.RingTheory.GradedAlgebra.FiniteType                                 instructions    96.6%
+ ~Mathlib.RingTheory.Ideal.Norm.RelNorm                                       instructions   -13.3%
+ ~Mathlib.RingTheory.IntegralClosure.IntegralRestrict                         instructions    -5.4%
+ ~Mathlib.RingTheory.Jacobson.Ring                                            instructions   -23.8%
+ ~Mathlib.RingTheory.Kaehler.Basic                                            instructions    -6.3%
+ ~Mathlib.RingTheory.Kaehler.Polynomial                                       instructions   -31.8%
+ ~Mathlib.RingTheory.LaurentSeries                                            instructions   -14.3%
- ~Mathlib.RingTheory.LinearDisjoint                                           instructions    14.5%
- ~Mathlib.RingTheory.LittleWedderburn                                         instructions    27.9%
- ~Mathlib.RingTheory.LocalProperties.Projective                               instructions    31.1%
+ ~Mathlib.RingTheory.LocalRing.ResidueField.Ideal                             instructions   -40.5%
+ ~Mathlib.RingTheory.Localization.Free                                        instructions   -31.9%
- ~Mathlib.RingTheory.Polynomial.Cyclotomic.Basic                              instructions    28.2%
+ ~Mathlib.RingTheory.Polynomial.Quotient                                      instructions   -28.4%
- ~Mathlib.RingTheory.Presentation                                             instructions    25.6%
+ ~Mathlib.RingTheory.RingHom.Locally                                          instructions   -17.1%
+ ~Mathlib.RingTheory.Spectrum.Prime.Homeomorph                                instructions   -20.7%
+ ~Mathlib.RingTheory.Spectrum.Prime.Polynomial                                instructions   -19.7%
- ~Mathlib.RingTheory.TensorProduct.Basic                                      instructions     3.2%
+ ~Mathlib.RingTheory.Valuation.AlgebraInstances                               instructions   -58.8%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                               instructions   -49.3%
- ~Mathlib.RingTheory.WittVector.FrobeniusFractionField                        instructions    49.9%
- ~Mathlib.SetTheory.Game.Basic                                                instructions    14.7%
- ~Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits                       instructions    57.0%
- ~Mathlib.Topology.ContinuousMap.StoneWeierstrass                             instructions    16.6%

[Matthew Ballard]

(deleted)

[Matthew Ballard]

/poll Should we
Go with deprioritizing CommX.toX (first diff above)
Go with prioritizing CommX.toX(most recent diff above)
Do nothing and see any core fix is inbound

[Matthew Ballard]

I think the first option is reasonable for the short term and can easily be ripped out if we want to unbundle Comm from everything.