Philosophical question: having two definitions for transi...

Stream: mathlib4

[Kenny Lau]

This is a general philosophical question, maybe even a bit of an XY-problem, sometimes people want to change the definition of X from A to B, but X is used in a lot of files, so the PR would be literally impossible.

(eg the recent “computable polynomial” discussion, or changing the non singular condition for elliptic curves)

is it possible to keep X using A, and build a “duplicate” Y using B (so the PR will be tiny), and then gradually deprecate A and transition to B? we can add a tag to stop new definitions from using A, or something like that?

[Damiano Testa]

I think that my main concern with this is that you cannot really enforce that the refactor gets to completion, unless it is completed in the first place.

[Damiano Testa]

I would worry that it is very easy for the situation to be that you are halfway through the replacement and suddenly no one has the capacity to continue.

[Damiano Testa]

At that point, no one can develop the old version, no one is developing the new one and the situation is worse than at the start.

[Damiano Testa]

By the way, this is also one of the reasons why I started a few times, but never finished making AddMonoidAlgebra into a structure containing a Finsupp.

[Kevin Buzzard]

The PR is not impossible at all, it was only a couple of months ago that I reviewed and merged a gigantic PR touching hundreds of files which completely changed the way that the order hierarchy interacted with the algebra hierarchy.

[Matthew Ballard]

Not impossible but the activation energy is pretty high. We still haven’t seen decoupling of the Analysis and Algebra hierarchies started right?

[Artie Khovanov]

The order-algebra PR was a very good idea by the way! Made some stuff I'm working on downstream much easier to state, because I wanted to consider whether a ring could be ordered.

[Raghuram]

Maybe one solution (at least in some cases) would be to first ensure that the interface to X doesn't expose the fact that it is defined as A (and if ensuring this requires changes, merge those changes first), then reimplement X and its interface using B. This solves what seems to me like the main problem with working on transitioning from A to B for a long time: that if new code written while definition B is being written uses X in a way that relies on definition A then "completing the refactor" becomes a moving target.