Zulip Chat Archive

#23755 is the second of three steps in splitting Algebra.Order.GroupWithZero.Unbundled to remove another long file. It doesn't actually split, it just renames the file (and another one) to something more sensible

Jeremy Tan (Apr 07 2025 at 13:30):

:up:

Kim Morrison (Apr 07 2025 at 13:45):

Jeremy Tan said:

:up:

@Jeremy Tan, please don't ping so quickly, it's just noise, and if anything makes it less likely you'll get quick attention to PRs.

Jeremy Tan (Apr 11 2025 at 00:16):

#23928 clears deprecations from 1 to 10 October 2024 (which is a lot)

Jeremy Tan (Apr 11 2025 at 00:40):

I still have #23686 open, that fixes a bunch of induction branch names and motives

Jeremy Tan (Apr 11 2025 at 02:52):

And I would like #23860 (MeasureTheory.Integral.Lebesgue.Basic) merged first before I split the last two long files

Jeremy Tan (Apr 12 2025 at 00:02):

#23324 (depriming induction' with 5+ variables) is now unblocked

Jeremy Tan (Apr 12 2025 at 00:05):

As is #23947 (prove lintegral_eq_zero_iff' without monotone convergence, so as to help #23860)

Jeremy Tan (Apr 12 2025 at 00:08):

And #23936, which clears up files with no declarations or only deprecated ones

Jeremy Tan (Apr 15 2025 at 12:57):

#24079 replaces (almost) all instances of dot-space-space with dot-space (single sentence spacing)

Yaël Dillies (Apr 15 2025 at 13:00):

Some people like to separate their sentences with two spaces. What's the issue with that?

Jeremy Tan (Apr 15 2025 at 13:02):

Yaël Dillies said:

Some people like to separate their sentences with two spaces. What's the issue with that?

Every major English style guide says no to two spaces

Michael Rothgang (Apr 15 2025 at 13:43):

Before accepting such a change, I (personally) would like to see some consensus that this is desirable (and a PR to the style guide). This looks like a substantial bikeshedding hub, let's agree on it before making the change :-)

Jeremy Tan (Apr 15 2025 at 14:04):

I did this once for my own amusement, without intention of having this merged. I have made this PR partly to save the trouble of doing this again

Kevin Buzzard (Apr 15 2025 at 17:33):

And to cause trouble to all the people who will get merge conflicts as a result.

Kevin Buzzard (Apr 15 2025 at 17:34):

which is far more trouble than running a regex search on mathlib.

Kim Morrison (Apr 16 2025 at 00:36):

Yes, let's not do this.

Eric Wieser (Apr 16 2025 at 01:15):

I think there was a related proposal recently to use semantic line breaking, where every . is followed by a newline

Eric Wieser (Apr 16 2025 at 01:15):

(Which gives better git diffs than column wrapping, and is less
less likely to accidentally repeat a word)

Jeremy Tan (Apr 16 2025 at 02:05):

#16408 (revived) deprecates Order.Nat

Jeremy Tan (Apr 23 2025 at 00:04):

#24282 renames Lintegral, Laverage to LIntegral, LAverage (following AEStronglyMeasurable)

Jeremy Tan (May 01 2025 at 00:17):

#24483 clears the remaining deprecations from October 2024

Yaël Dillies (May 01 2025 at 06:09):

Can we please seriously consider a bot writing and merging those PRs?

Jeremy Tan (May 01 2025 at 06:13):

Yaël Dillies said:

Can we please seriously consider a bot writing and merging those PRs?

The regex can't clear out everything, manual intervention will always be needed (unlike updating dependencies)

Jeremy Tan (May 01 2025 at 06:13):

Also I don't know how to write a bot

Yaël Dillies (May 01 2025 at 06:29):

Sure, but the bot can still do most of the work, no?

Michael Rothgang (May 01 2025 at 08:59):

Task 37 from #mathlib4 > Call for help: technical/ organisational debt sounds like a fun one to pick up. Perhaps it can be regex-automated, it would certainly make mathlib nicer to read.

Damiano Testa (May 01 2025 at 11:26):

Jeremy Tan said:

Yaël Dillies said:

Can we please seriously consider a bot writing and merging those PRs?

The regex can't clear out everything, manual intervention will always be needed (unlike updating dependencies)

It need not be a regex, it could be a syntax-aware replacement. Looking at the PR, all the declaration removals could have been automated correctly, I think. The section removal could also be automated, but for that it would maybe be better if the name of the section included a date, so that the bot would know to remove it.

Yaël Dillies (May 01 2025 at 12:06):

I think empty sections can simply be another job? Removing deprecations isn't the only way to end up with an empty section

Jeremy Tan (May 02 2025 at 00:26):

In any case, I don't know how to get the bot to automatically create a PR to remove deprecations. We should start with just the regex, then see how to turn it into a syntax-aware job

Notification Bot (May 02 2025 at 00:26):

A message was moved here from #PR reviews > #24452 + #24454 + #24506: rotate_isos tactic by Jeremy Tan.

Jeremy Tan (May 03 2025 at 07:52):

#23676 has been updated to use the new single-case induction syntax

Jeremy Tan (May 03 2025 at 08:06):

As has #23324

Jeremy Tan (May 20 2025 at 05:40):

IMO 2001 Q4: #25036

Jeremy Tan (May 21 2025 at 01:32):

IMO 2001 Q3: #25068

Jeremy Tan (May 23 2025 at 01:53):

#25124 provides the formula for the number of edges in the Turán graph (something I had tried to do when first proving the theorem, as some proofs go through the formula)

Jeremy Tan (May 23 2025 at 03:17):

#25126 deprimes Computability.TuringDegree

Jeremy Tan (May 23 2025 at 03:56):

#25127 deprimes MeasureTheory and Probability

Jeremy Tan (May 24 2025 at 02:38):

And now I'd like another look at #23676. I have removed the rename_is in favour of the new "arrowless" induction syntax

Jeremy Tan (May 26 2025 at 01:09):

#25198 deprimes Computability, FieldTheory, Combinatorics (1) and Control (1)

Jeremy Tan (Jun 06 2025 at 02:36):

#25353 deprimes induction in GroupTheory

Jeremy Tan (Jun 06 2025 at 03:15):

#25512 deprimes induction in Archive and SetTheory

Jeremy Tan (Jun 09 2025 at 06:15):

#25774 deprimes induction in CategoryTheory and AlgebraicTopology

Jeremy Tan (Jun 12 2025 at 09:13):

Migrating my PRs now…

#25770 - h-recursors
#25774 - deprime-algtop-cattheory
#25776 - deprime-analysis
#25783 - imo1985q2
#25785 - imo2001q3
#25786 - imo2001q4
#25788 - turangraph_count
#25790 - del-in-deprecated

Jeremy Tan (Jun 12 2025 at 13:43):

All migrated and updated – would like reviews on all of them

Eric Wieser (Jun 14 2025 at 13:21):

Could you add the migration label to them?

Jeremy Tan (Jul 07 2025 at 01:12):

@Eric Wieser I already did.

#25786 formalises IMO 2001 Q4

Jeremy Tan (Jul 07 2025 at 01:17):

#25770 fixes many induction branch names

Jeremy Tan (Jul 07 2025 at 01:20):

#25776 deprimes induction in Analysis

Jeremy Tan (Jul 07 2025 at 01:24):

#25774 deprimes induction in AlgebraicTopology and CategoryTheory

Jeremy Tan (Jul 07 2025 at 01:27):

#25790 deletes some files in the Deprecated folder (>6 months)

Jeremy Tan (Jul 16 2025 at 00:59):

#27185 renames the hypothesis names of four Submonoid recursors to fit the naming convention (this was found when formalising IMO 1997 Q3)

Jeremy Tan (Jul 16 2025 at 02:24):

#25770 (which fixes more recursor hypothesis names) has been sitting there for a month now without any action

Jeremy Tan (Jul 16 2025 at 02:24):

#27159 is the actual formalisation of IMO 1997 Q3

Jeremy Tan (Jul 29 2025 at 16:16):

#25774 (depriming induction in AlgebraicTopology and CategoryTheory) has just been bumped to resolve a merge conflict

Jeremy Tan (Aug 04 2025 at 12:17):

#27922 deprecates div_eq_iff_mul_eq and eq_div_iff_mul_eq (one is entirely equivalent to a tagged lemma, the other is equivalent to a tagged lemma plus eq_comm)

Jeremy Tan (Aug 30 2025 at 06:09):

#29123 and #29124 remove induction' in some (disjoint) files of the Data folder
#29125 removes Deprecated.Order which is now more than 6 months old

Jeremy Tan (Aug 30 2025 at 06:54):

#29127 removes induction' in about 5/12 of the files of RingTheory containing it

Kim Morrison (Sep 02 2025 at 03:15):

Jeremy Tan said:

#27922 deprecates div_eq_iff_mul_eq and eq_div_iff_mul_eq (one is entirely equivalent to a tagged lemma, the other is equivalent to a tagged lemma plus eq_comm)

Conflicted.

Jeremy Tan (Sep 03 2025 at 04:26):

#29123 (Data.{*Nat, Int, *Real})

Jeremy Tan (Sep 03 2025 at 04:27):

#29285 (RingTheory except 6 files)

Jeremy Tan (Sep 03 2025 at 04:27):

#29286 (Algebraexcept Polynomial subfolder)

Jeremy Tan (Sep 03 2025 at 04:28):

#29124 (Data.*Fin*)

Jeremy Tan (Sep 03 2025 at 04:29):

The plan is that once the second and third PRs above are merged I will make another PR depriming the rest of Algebra and RingTheory and all the new instances of induction' outside the Data, Algebra, RingTheory folders that appeared since the first round of depriming

Jeremy Tan (Sep 03 2025 at 04:30):

This will leave all remaining uses of induction' in Data

Jeremy Tan (Sep 03 2025 at 06:53):

#29289 chore: fix recursor names for Cycle.induction_on

Jeremy Tan (Sep 03 2025 at 07:20):

Jeremy Tan said:

The plan is that once the second and third PRs above are merged I will make another PR depriming the rest of Algebra and RingTheory and all the new instances of induction' outside the Data, Algebra, RingTheory folders that appeared since the first round of depriming

This will be #29291

Jeremy Tan (Sep 03 2025 at 13:26):

#29313 chore: deprime induction in Data.List (for real)

Jeremy Tan (Sep 10 2025 at 23:29):

I have had to update #29313 to resolve a merge conflict. Can someone have a look and maintainer merge this please?

Jeremy Tan (Sep 11 2025 at 02:49):

Merge conflicts for #29123 and #29124 have been fixed. I'd like them to be re-sent to bors

Jeremy Tan (Sep 11 2025 at 04:19):

#29291 is ready now

Jeremy Tan (Sep 11 2025 at 05:20):

#29537 fixes induction recursor names in two Algebra.Polynomial files (and deprimes their uses)

Jeremy Tan (Sep 11 2025 at 08:10):

#29542 deprimes the last uses of induction'

Last updated: Dec 20 2025 at 21:32 UTC